JKind v1.4.4

Fixes

• Bug fix: type check assertions. Prior to this, no type checking was being performed on assertions! (Thanks to Pooya Rahimian for finding this bug)
• Fixed a bug with assertions and interval generalization (Thanks to John Backes for finding this bug)
• Fixed a bug in the treatment of integer valued real literals in the JKind API (Thanks to John Backes for finding this bug)

Features

• Added 'mod' operator
• Changed the naming of inlined variables to show more structure

JKind v1.4.3

Major Features

• Support for interval generalization of counterexamples via the -interval command line flag. This is based on work by John Backes.
• Support for condact expressions.

Minor Features

• Now generates invariant candidates of the form 'x >= 0' for non-combinatorial variables x. This should cover many common invariants when using counters and timers.
• Improved the layout of counterexamples in the console output.
• Disabled integer division by negative numbers due to inconsistent interpretations between solvers.
• Allow -no_inv_gen and -reduce_inv flag together since even without automatic invariant generation, properties may be used as invariants to each other and thus invariant reduction still makes sense.

JKind v1.4.2

This release fixes a Lustre parsing performance issue by upgrading to ANTLR 4.1

JKind v1.4.1

The primary feature of this release is that sub-node properties are now lifted to top-level properties. The names will be mangled due to node inlining. The particular format of the mangled names is subject to change in the future.

Various small fixes and improvements have also been made.

JKind v1.4

Note: Batch files and shell scripts have been updated for this release.

New Features

• Support for record types (example)
• Addition of JLustre2Kind and JLustre2Excel as official parts of JKind
• Support for --%MAIN annotation to designate main Lustre node in a file
• Support for assertions over any variables (not just inputs as before)
• Warnings for algebraic loops and unguarded pres
• Various bug fixes
• Addition of the JKind API, see below

Introducing the JKind API

The JKind API is a Java API for interacting with JKind (and eventually other versions of Kind). It comes as jkind-api.jar in the JKind zip file. The API provides:

• A Lustre AST with pretty printer
• A wrapper around calling JKind (over the command line)
• Parsing and processing of XML results into a Java data structure
• JFace components for real time visualization of JKind results
• Excel output for overall results or individual counterexamples

See the examples for usage information.

JKind v1.3.1

JKind v1.3.1

• Various bug fixes
• Faster performance for z3

JKind v1.3

Old release

JKind and Lustre2excel v1.2

Old release

JKind and Lustre2excel v1.1

Old release

JKind v1.0

Old release