loonwerks/jkind

JKind - An infinite-state model checker for safety properties in Lustre

JKind

JKind is an SMT-based infinite-state model checker for safety properties in Lustre. JKind uses parallel cooperating engines including k-induction, property directed reachability, and template-based invariant generation.

Downloads

JKind is written in Java and requires at least Java 8. The latest release of JKind is available on the releases page. This includes the JKind model checker as well as the JRealizability, JLustre2Excel, and JLustre2Kind tools.

Design Goals

JKind is designed to be cross-platform, reliable, and easy to extend. Power and performance are secondary goals. Additionally, JKind attempts to be mostly compatible with pkind and Kind 2, though this varies over time due to developments in both systems.

Alternative Solvers (optional)

By default, JKind is packaged with SMTInterpol as its underlying SMT solver. Advanced users may wish to install alternative solvers such as Z3, Yices (version 1), Yices 2, CVC4, or MathSAT.

Minimal IVCs enumeration (optional)

JKind supports enumeration of All Minimal Inductive Validity Cores (All-MIVCs) to provide a full enumeration of all minimal set of model elements necessary for the inductive proofs of a safety property. Both the offline enumeration (as described in [1]) and the online enumeration (as described in [2]) have been implemented, and the offline enumeration is the algorithm made available for general use. To use the MIVC enumeration, run JKind with the following arguments:

-all_ivcs -solver z3

In addition, use the -timeout argument to limit the time for the enumeration, e.g.,

-timeout 1800

[1] E. Ghassabani, M. W. Whalen, and A. Gacek. Efficient generation of all minimal inductive validity cores. 2017 Formal Methods in Computer Aided Design (FMCAD), pages 31–38, 2017. [2] J. Bendik, E. Ghassabani, M. Whalen, and I. Cerna. Online enumeration of all minimal inductive validity cores. In International Conference on Software Engineering and Formal Methods, pages 189–204. Springer, 2018.

jkind's Issues

SmtLib2 Parser does not work for z3 models

Current z3 (version 4.8.11) creates models which do not start with '(model ` which is defined in the grammar for smtlib.

bmc process failed                                                                                                                                                                           
jkind.JKindException: Solver output parse error line 2:2 missing 'model' at '('                                                                                                              
        at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13)       
...

I think this is also what the SMTlib documentation specifies.

c.f. https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-r2015-06-28.pdf

(get-model) returns a list (d1 · · · dk) of definitions specifying all and only the current user declared function symbols {g1, . . . , gm} in the current model A.

Bug in inlining

This property should be true, but it's shown as false due to a bug in node inlining.

https://gist.github.com/agacek/4876961

Null Pointer Exceptions

java.lang.NullPointerException
at jkind.solvers.yices.YicesModel.getFunctionValue(YicesModel.java:69)
at jkind.processes.Director.extractSignal(Director.java:284)
at jkind.processes.Director.extractCounterexample(Director.java:272)
at jkind.processes.Director.processMessages(Director.java:218)
at jkind.processes.Director.run(Director.java:88)
at jkind.JKind.main(JKind.java:47)
at jkind.Main.main(Main.java:47)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(Unknown Source)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(Unknown Source)
at java.lang.reflect.Method.invoke(Unknown Source)
at org.eclipse.jdt.internal.jarinjarloader.JarRsrcLoader.main(JarRsrcLoader.java:58)

F:\runtime-LimpEmbedded\testLimp>jkind -version
JKind 1.4.5

Please see your Gmail account for a Lustre file that elicits the bug.

Error in Column AA (Step 25) in jlustre2excel Output

Column AA — which corresponds to the 25th step — in jlustre2excel's output appears to be consistently incorrect.

For example, for this Lustre,

node triggers(a : bool; b : bool) returns (holds : bool);
let
   holds = (b and (a or (false -> (pre holds))));
tel;

The spreadsheet generated has the following formulas for Z, AA, and AB:

=IF(OR(IF(ISERROR(Y7),FALSE,Y7=""),IF(ISERROR(Z3),FALSE,Z3=""),IF(ISERROR(Z4),FALSE,Z4="")),"",AND(Z4,OR(Z3,(Y7))))
=IF(OR(IF(ISERROR(AA3),FALSE,AA3=""),IF(ISERROR(AA4),FALSE,AA4=""),IF(ISERROR(Z7),FALSE,Z7="")),"",AND(AA4,OR(AA3,(Z7))))
=IF(OR(IF(ISERROR(AA7),FALSE,AA7=""),IF(ISERROR(AB3),FALSE,AB3=""),IF(ISERROR(AB4),FALSE,AB4="")),"",AND(AB4,OR(AB3,(AA7))))

Nearly every cell reference in column AA is incorrect.

Note — Excel identifies this problem immediately with its "this cell's formula doesn't match its neighbors" warning, which is frankly one of the cleverest things I've ever seen Microsoft do. No heroics on my part, here. :)

Allow constant expressions in subrange types

It would be nice if JKind allowed constant expressions in subrange types, e.g.

const N = 10;
...
x : subrange [N, N+3] of int;

Counterexample truncation sign error in stdout

Truncated values can have the wrong sign when printed to stdout. The values are represented correctly (confirmed with xls output) but the truncation used causes small negative values to be represented as positive. E.g. a value of -0.00045 was represented as 0.000* instead of -0.000*

Z3 parse error during division

Division operations fail when using non-constant values with Z3 versions 4.8.9+

bmc process failed
jkind.JKindException: Solver output parse error line 80:14 no viable alternative at input '/'
        at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13)
        at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:67)
        at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:561)
        at org.antlr.v4.runtime.DefaultErrorStrategy.reportNoViableAlternative(DefaultErrorStrategy.java:310)
        at org.antlr.v4.runtime.DefaultErrorStrategy.reportError(DefaultErrorStrategy.java:147)
        at jkind.solvers.smtlib2.SmtLib2Parser.id(SmtLib2Parser.java:633)
        at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:139)
        at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:86)
        at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:219)
        at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:208)
        at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:72)
        at jkind.engines.BmcEngine.checkProperties(BmcEngine.java:48)
        at jkind.engines.BmcEngine.main(BmcEngine.java:39)
        at jkind.engines.Engine.run(Engine.java:36)
        at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
        at java.lang.Thread.run(Unknown Source)
k-induction process failed
jkind.JKindException: Solver output parse error line 80:14 no viable alternative at input '/'
        at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13)
        at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:67)
        at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:561)
        at org.antlr.v4.runtime.DefaultErrorStrategy.reportNoViableAlternative(DefaultErrorStrategy.java:310)
        at org.antlr.v4.runtime.DefaultErrorStrategy.reportError(DefaultErrorStrategy.java:147)
        at jkind.solvers.smtlib2.SmtLib2Parser.id(SmtLib2Parser.java:633)
        at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:139)
        at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:86)
        at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:219)
        at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:208)
        at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:72)
        at jkind.engines.KInductionEngine.checkProperties(KInductionEngine.java:88)
        at jkind.engines.KInductionEngine.main(KInductionEngine.java:53)
        at jkind.engines.Engine.run(Engine.java:36)
        at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
        at java.lang.Thread.run(Unknown Source)
invariant-generation process failed
jkind.JKindException: Solver output parse error line 80:14 no viable alternative at input '/'
        at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13)
        at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:67)
        at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:561)
        at org.antlr.v4.runtime.DefaultErrorStrategy.reportNoViableAlternative(DefaultErrorStrategy.java:310)
        at org.antlr.v4.runtime.DefaultErrorStrategy.reportError(DefaultErrorStrategy.java:147)
        at jkind.solvers.smtlib2.SmtLib2Parser.id(SmtLib2Parser.java:633)
        at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:139)
        at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:86)
        at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:219)
        at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:208)
        at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:72)
        at jkind.engines.invariant.AbstractInvariantGenerationEngine.refineBaseStep(AbstractInvariantGenerationEngine.java:74)
        at jkind.engines.invariant.AbstractInvariantGenerationEngine.main(AbstractInvariantGenerationEngine.java:49)
        at jkind.engines.Engine.run(Engine.java:36)
        at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
        at java.lang.Thread.run(Unknown Source)

JKind prevents use of non-constant multiplication/division, regardless of solver

The Z3 solver supports non-constant multiplication (in an incomplete form - it may return "unknown"), but JKind will still reject any non-linear expressions when Z3 is selected as the solver.

Could JKind be updated to allow non-linear multiplication and division if the Z3 solver is being used?

Thanks!

Report invariants used

It would be nice if JKind had an option to report the invariant lemmas which were necessary to prove a given property. This would require extra checking (removing unused lemmas) but could be very useful for users.

Z3 may produce invalid counter-examples

I noticed that JKind was reporting counter-examples where the variable values made no sense. Looking at the scratch file, it seems that Z3 returned an "unknown", but since it was able to produce a model still, JKind reported that model as a counter-example.

For an example model that produces this effect:
http://greggay.com/tmp/injected_model.lus
http://greggay.com/tmp/injected_model.lus.base.smt2

Unsound interaction between arrays and subranges

I was trying to understand the semantics of arrays as implemented in jkind, and I came across an example, where just adding an additional property to prove causes jkind to change its mind about the validity of another property:

type T = subrange [2,2] of int;
  
node main() returns ();
var a : T[2];
    j : T;
    i : int;
    ok1, ok2 : bool;
let
  a   = [2,2];
  i   = 3;
  j   = a[i];
  ok1 = a[i] = 2;
  ok2 = j = 2;
  --%PROPERTY ok1;
  --%PROPERTY ok2;
tel

If you run the example as is, then jkind states the both properties are valid. If you comment out the last line (where we ask it to prove ok2), then it reports that ok1 is invalid.

This is with version 4.0.1

As an aside: what is the intended treatment of "undefined" values---is is an arbitrary value of the given type, or is it some special additional element that is different from all elements in the type?

Arithmetic Exception

Attached model exercises an arithmetic exception.

Solver = Z3 (4.7.1)
JKind (latest commit from master, em in an Eclipse tool)

error.txt

The declaration of a constant with struct type

I have two examples.

Example 1:
type sPos_t = int[4];
const A : int = 1;
const B : int = 2;
const INVALID_SPOS : sPos_t = [A,B,A,B];

node main (inpu: sPos_t)
returns (outp: bool);
let
outp = INVALID_SPOS[2] <> 0;
--%PROPERTY outp;
tel;

---

Example 2:
type sPos_t = struct {iIdx: int; iAbs: int};
const A : int = -1;
const B : int = 0;
const INVALID_SPOS : sPos_t = {iIdx := A; iAbs := B};
--const INVALID_SPOS : sPos_t = {A; B};

node main (varia: sPos_t)
returns(Outp: bool);
let
Outp = INVALID_SPOS.A > 0;
--%PROPERTY Outp;
tel;

---

The first example is correct, while the second example is wrong with the following error.
Parse error line 4:30 no viable alternative at input '{' const INVALID_SPOS : sPos_t = {iIdx := A; iAbs := B};

Parse error line 4:42 extraneous input 'iAbs' expecting {<EOF>, 'const', 'node', 'type', 'function'} const INVALID_SPOS : sPos_t = {iIdx := A; iAbs := B};

In the grammar of Luster, it is ok.
In this situation, I do not care whether the property is valid or not.
So, I was wondering if jkind supports the definition of constant with struct type.
Or maybe I wrote the wrong sentence in example 2. Who can solve my question?

Z3-related crash regarding parsing Solver output

JKind is crashing on the provided example model (you will have to unzip error.zip and run error.lus to reproduce the error.

jkind -solver z3 -smooth -no_slicing error.lus

This produces the following error:

This is using JKind version 4.0.1 and Z3 4.7.1. The error was reproduced on JKind 4.0.1 and Z3 4.6.0 and 4.6.2.

error.zip

If an unknown identifier appears in a property, JKind will throw an NPE rather than yielding a descriptive error.

<lgwagner@jepsen:~/patterns/microwave>jkind microwave.lus
Exception in thread "main" java.lang.NullPointerException
at java.util.AbstractCollection.addAll(Unknown Source)
at jkind.slicing.LustreSlicer.getPropertyDependencies(LustreSlicer.java:24)
at jkind.slicing.LustreSlicer.slice(LustreSlicer.java:17)
at jkind.Main.main(Main.java:49)

Please ask me for my microwave.lus file that exhibits the error.

Non-constant division

The non-constant division is a bit restrictive. Is there a way to by-pass this? Maybe via an option.

jkind --xml_to_stdout -main AltitudeControl_Demo_SAFETY_REQUIREMENT_1 AltitudeControl_Demo.lus

AltitudeControl_Demo.lus.zip

PDR soundness bug with assertions

PDR handles assertions in an unsound way. The following property should be false but PDR proves it.

node main(x : bool) returns ();
let
  assert true -> pre x;
  --%PROPERTY x;
tel;

Flag unguarded pre results in counterexamples

We already provide a warning for unguarded pre expressions as part of our static analysis. For a solver like yices we should be able to detect when a counterexample relies on values before the initial time step. We should think about reporting this information to the user. (Suggested by Dan DaCosta)

Inductive Counterexample

pKind supports an inductive counterexample which can be useful to determine which invariant is necessary to prove a property.

Is this easy to support?

smtlib2 parse error

jkind --version

JKind 4.0.0
Detected solvers: smtinterpol, z3, yices, yices2, cvc4, mathsat

command:

jkind -xml -solver z3 -timeout 16 --no_slicing fuzz.lus

exception:

jkind.JKindException: Solver output parse error line 8368:5 missing {'/', '>=', '<', '=', '>', '<=', 'and', 'ite', 'not', '-'} at 'or'
at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13)
at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:67)
at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:561)
at org.antlr.v4.runtime.DefaultErrorStrategy.reportMissingToken(DefaultErrorStrategy.java:409)
at org.antlr.v4.runtime.DefaultErrorStrategy.singleTokenInsertion(DefaultErrorStrategy.java:512)
at org.antlr.v4.runtime.DefaultErrorStrategy.recoverInline(DefaultErrorStrategy.java:476)
at jkind.solvers.smtlib2.SmtLib2Parser.fn(SmtLib2Parser.java:339)
at jkind.solvers.smtlib2.SmtLib2Parser.body(SmtLib2Parser.java:290)
at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:153)
at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:83)
at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:208)
at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:198)
at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:63)
at jkind.engines.KInductionEngine.checkProperties(KInductionEngine.java:88)
at jkind.engines.KInductionEngine.main(KInductionEngine.java:53)
at jkind.engines.Engine.run(Engine.java:35)
at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
at java.lang.Thread.run(Thread.java:745)

fuzz.lus:

fuzz.txt

Allow proposed invariants

JKind should support proposed invariants, e.g.

--%INVARIANT inv0;

These are slightly different than properties:

1. We don't report if they are true or unknown
2. We report some kind of warning if they are false
3. We slice away invariants which are not related to the properties of interest
4. We should probably treat subrange declarations on locals and outputs as these types of invariants

But these invariants should be handled by the base and inductive step processes rather than the invariant generation process. These are things we expect to be true and perhaps useful, so we want them checked quickly. Invariant generation is more speculative and takes longer to run.

Large rationals are expressed as hard to interpret fractions

Is it possible to have a flag that will print rationals as decimal points with some predetermined number of significant figures, rather than very huge fractions which are hard to interpret within counterexamples.

For example: -23432423423/23477234732442 is hard to read.

Array assignment

There are two arrays: inp: int[50] and p: int[20]. I was wondering whether it is possible to split the first 20 elements of inp and assign them to p.
Further, if it is possible, how about assign the first 20 elements of inp to p in one cycle?
Sometimes, this kind of assignment is very useful and important.

node main (inp: int[50])
returns (outp: bool);
var
p: int[20];
let
p = (pre p)[0 := pre inp[0]];
outp = (p[10] <> 4) or (p[15] <> 5);
--%PROPERTY outp;
tel;

==========================================================
In Java, we can do that
for(int i = 0; i < p.length; i++){
p[i] = inp[i];
}
How can we do that in Lustre.

IfThenElse exprs cannot contain node calls, even if type correct

JKind does not support the following program, because the If then else expression assigning output1,output2 contains node call expressions. Current workaround is done by lifting the expressions.

node test_call(a : int) returns (x : int; y : int);
let
x = a + 1;
y = a - 1;
tel ;

node main (input : int; x : bool) returns (output1 : int; output2 : int);
let
output1,output2 =
if x
then test_call(input+1)
else test_call(input-1) ;
tel ;

JKind breaks with condacts in Java 9+

JKind 4.4.1 (and earlier) has an issue translating condacts when using Java 9+.

This issue is related the concurrent modification exception when using the computeIfAbsent method of Java maps. The issue is described here.

https://stackoverflow.com/questions/54824656/since-java-9-hashmap-computeifabsent-throws-concurrentmodificationexception-on

user specified precision in rational printing

provide a user flag to specify the precision of rationals.

I'm thinking: -precision INT

the INT argument will produce the underlying fraction if the argument is 0 or N places of precision in a decimal format (up to some reasonable level, like 9). I think we should default N to 3 so it mimics current behavior by default.

Notes:

• we used to provide a printout of the fractions that represented rationals but it became very hard to relate two values in a CEX (i.e. is 4388234/2342 > 2378823/273 ) which was easy to do for a couple of values but tedious for numerous values.
• loss of precision in the current method has its own drawbacks

incorrect scripts for Linux

In your releases, the files contain the ^M characters. I had to run the "dos2unix" utility to get them to work. You might want to fix that on your next release.

Jkind 2.1 requires Java 8

Version 2.1 seems to be built with Java 8 (classfile version 52.0). Is it possible to provide a build for Java 7?

Support for Casting

Yices does not support typecasting. However, other solvers - such as Z3 - do support casting from integer -> real and real -> integer.

If possible, could JKind be upgraded to support the Lustre cast(var, type) operation when using an appropriate solver?

As usual, thanks for your hard work.

JKind does not detect division by zero

JKind does not detect division by zero (using / or 'div'). Instead, it relies on the behavior of the underlying solver which is probably inconsistent and may result in error messages directly from the solver.

Since you can only divide by constants, we should be able to detect this statically. However, doing the detection requires writing code for evaluation of expression which is more work than I'm willing to do at the moment.

Thanks to Lucas Wagner for pointing this out.

Add support for '$' as an identifier character

JKind is often used for translation from other notations and one difficulty is that it is often necessary to introduce new identifiers during translation (along with the identifiers from the problem being translated). There is a risk of name clashes for the new identifiers. I would like to allow the use of the '$' character in identifiers to facilitate creating these fresh identifiers without name clashes.

Examples of valid identifiers with the addition:

foo$bar, $theOneRing x$

K-induction fails with SMTInterpol Exception

For the attached Lustre program, current jkind (1f836bb) fails with

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++                            
UNKNOWN PROPERTIES: [prop] || True for 17 steps || Time = 6.941s                          
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
                                                   
    -------------------------------------                                
    --^^--        SUMMARY          --^^--       
    -------------------------------------           
                           
UNKNOWN PROPERTIES: [prop]

k-induction process failed
de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Undeclared function symbol (ite Bool Real Int)
        at de.uni_freiburg.informatik.ultimate.logic.NoopScript.term(NoopScript.java:321)
        at de.uni_freiburg.informatik.ultimate.logic.NoopScript.term(NoopScript.java:296)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:83)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:58)
        at jkind.solvers.smtinterpol.SmtInterpolSolver.convert(SmtInterpolSolver.java:168)
        at jkind.solvers.smtinterpol.SmtInterpolSolver.assertSexp(SmtInterpolSolver.java:46)
        at jkind.engines.KInductionEngine.assertInvariants(KInductionEngine.java:126)
        at jkind.engines.KInductionEngine.assertNewInvariants(KInductionEngine.java:121)
        at jkind.engines.KInductionEngine.handleMessage(KInductionEngine.java:180)
        at jkind.engines.messages.InvariantMessage.accept(InvariantMessage.java:22)
        at jkind.engines.messages.MessageHandler.handleMessage(MessageHandler.java:30)
        at jkind.engines.messages.MessageHandler.processMessagesAndWaitUntil(MessageHandler.java:38)
        at jkind.engines.KInductionEngine.processMessagesAndWait(KInductionEngine.java:62)
        at jkind.engines.KInductionEngine.main(KInductionEngine.java:49)
        at jkind.engines.Engine.run(Engine.java:36)
        at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
        at java.lang.Thread.run(Thread.java:748)

catching the error and printing the Sexp gives

(not (<= (+ (ite false (/ (/ 0 1) (/ 1 1)) (ite $f_t0$0 (+ $p12$0 (/ (/ (- 0 94) 1) (/ 1 1))) (ite $f_t5$0 (+ $p12$0 (/ (/ (- 0 94) 1) (/ 1 1))) (ite $f_t6$0 (+ $p12$0 (/ (/ (- 0 1) 1) (/
1 1))) (ite $f_t7$0 (+ $p12$0 (/ (/ (- 0 1) 1) (/ 1 1))) (ite $f_t2$0 (+ $p12$0 (/ (/ 1 1) (/ 1 1))) (ite $f_t6$0 (+ $p12$0 (/ (/ 1 1) (/ 1 1))) $p12$0))))))) (/ (/ 1 1) (/ 1 1))) (/ (/ 0
1) (/ 1 1)))) 

problem.zip

jKind Starting Script (on a Mac)

Platform: Mac OS 10.11.3

I know you guys aren't officially supporting Mac but I wanted to let you know that we were having a problem in-house running the following script:

!/bin/sh

JKIND_PATH=$(readlink -e $0)
JKIND_DIR=$(dirname $JKIND_PATH)
java -jar $JKIND_DIR/jkind.jar -jkind "$@"

The command line in the terminal provides an illegal usage on readlink -f

On the Mac systems here, we are working around this issue by using the old starting script:

!/bin/sh

java -jar $(dirname $0)/jkind.jar -jkind "$@"

Stack Overflow

The attached file (renamed to a TXT file because Github will not accept a .lus extension) generates a stack overflow in JKind 2.2.1. It seems to be associated with the PDR process.

-------------------------------------
--^^--        SUMMARY          --^^--
-------------------------------------

VALID PROPERTIES: [high_turn_bound]

UNKNOWN PROPERTIES: [low_turn_bound]

pdr process failed
java.lang.StackOverflowError
at java.util.IdentityHashMap.hash(Unknown Source)
at java.util.IdentityHashMap.put(Unknown Source)
at de.uni_freiburg.informatik.ultimate.smtinterpol.util.IdentityHashSet.add(IdentityHashSet.java:51)
at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.UnsatCoreCollector.accept(UnsatCoreCollector.java:58)
at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.UnsatCoreCollector.visit(UnsatCoreCollector.java:70)
at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.UnsatCoreCollector.accept(UnsatCoreCollector.java:62)
at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.UnsatCoreCollector.visit(UnsatCoreCollector.java:70)
at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.UnsatCoreCollector.accept(UnsatCoreCollector.java:62)
at de.uni_freiburg.informatik.ultimate.smtinterpol.proof.UnsatCoreCollector.visit(UnsatCoreCollector.java:70)

TicTacToe.spear.lus.txt

Yices output parser appears broken...

I got this error on our microwave model. I can't find a place to upload the associated file, else I would.

<lgwagner@tiryns:~/atc/training/models>jkind microwave.kind.lus

JAVA KIND

There are 13 properties to be checked.
PROPERTIES TO BE CHECKED: [s1, r1, r3, r4, s2, r7, r8, r2, r5, r6, r10, r11, r12]

line 29:10 extraneous input '60' expecting ')'
line 19:10 extraneous input '60' expecting ')'
line 20:10 extraneous input '10' expecting ')'
line 30:10 extraneous input '10' expecting ')'
line 75:10 extraneous input '1' expecting ')'
line 76:11 extraneous input '1' expecting ')'
line 124:11 extraneous input '1' expecting ')'
line 125:10 extraneous input '1' expecting ')'
line 126:10 extraneous input '1' expecting ')'
-------------------------------------
--^^-- SUMMARY --^^--
-------------------------------------

UNKNOWN PROPERTIES: [s1, r1, r3, r4, s2, r7, r8, r2, r5, r6, r10, r11, r12]

Inductive process failed
jkind.JKindException: Error parsing Yices output
at jkind.solvers.YicesSolver.parseYices(YicesSolver.java:129)
at jkind.solvers.YicesSolver.readResult(YicesSolver.java:114)
at jkind.solvers.YicesSolver.query(YicesSolver.java:84)
at jkind.solvers.YicesSolver.query(YicesSolver.java:67)
at jkind.processes.InductiveProcess.checkProperties(InductiveProcess.java:99)
at jkind.processes.InductiveProcess.main(InductiveProcess.java:46)
at jkind.processes.Process.run(Process.java:47)
at java.lang.Thread.run(Thread.java:722)
Invariant process failed
jkind.JKindException: Error parsing Yices output
at jkind.solvers.YicesSolver.parseYices(YicesSolver.java:129)
at jkind.solvers.YicesSolver.readResult(YicesSolver.java:114)
at jkind.solvers.YicesSolver.query(YicesSolver.java:84)
at jkind.solvers.YicesSolver.query(YicesSolver.java:67)
at jkind.processes.InvariantProcess.refineBaseInvariants(InvariantProcess.java:129)
at jkind.processes.InvariantProcess.basePhase(InvariantProcess.java:114)
at jkind.processes.InvariantProcess.main(InvariantProcess.java:60)
at jkind.processes.Process.run(Process.java:47)
at java.lang.Thread.run(Thread.java:722)
<lgwagner@tiryns:~/atc/training/models>

Output parse error when using Z3

Ran into a problem when using Z3 with FuzzM, I think it is a problem with JKind's output parsing for newer versions of Z3. I was able to reproduce on JKind 4.4.0 (FuzzM uses a vendored copy of JKind 4.0.0).

Here's the file that FuzzM ends up calling JKind on (note that I had to upload it as a .txt file because GitHub didn't like the .lus extension).
fuzz.txt

Here's the command I called and the output:

$ java -jar jkind/build/libs/jkind.jar -jkind -xml -solver z3 --no_slicing fuzz.txt
==========================================
  JKind 4.4.0
==========================================

There are 1 properties to be checked.
PROPERTIES TO BE CHECKED: [___fuzzProperty]

    -------------------------------------
    --^^--        SUMMARY          --^^--
    -------------------------------------

UNKNOWN PROPERTIES: [___fuzzProperty]

bmc process failed
jkind.JKindException: Solver output parse error line 634:4 missing 'define-fun' at 'x!1'
	at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13)
	at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:67)
	at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:561)
	at org.antlr.v4.runtime.DefaultErrorStrategy.reportMissingToken(DefaultErrorStrategy.java:409)
	at org.antlr.v4.runtime.DefaultErrorStrategy.singleTokenInsertion(DefaultErrorStrategy.java:512)
	at org.antlr.v4.runtime.DefaultErrorStrategy.recoverInline(DefaultErrorStrategy.java:476)
	at org.antlr.v4.runtime.Parser.match(Parser.java:223)
	at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:165)
	at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:102)
	at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:221)
	at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:210)
	at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:72)
	at jkind.engines.BmcEngine.checkProperties(BmcEngine.java:48)
	at jkind.engines.BmcEngine.main(BmcEngine.java:39)
	at jkind.engines.Engine.run(Engine.java:36)
	at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
	at java.base/java.lang.Thread.run(Thread.java:832)
k-induction process failed
jkind.JKindException: Solver output parse error line 634:4 missing 'define-fun' at 'x!1'
	at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13)
	at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:67)
	at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:561)
	at org.antlr.v4.runtime.DefaultErrorStrategy.reportMissingToken(DefaultErrorStrategy.java:409)
	at org.antlr.v4.runtime.DefaultErrorStrategy.singleTokenInsertion(DefaultErrorStrategy.java:512)
	at org.antlr.v4.runtime.DefaultErrorStrategy.recoverInline(DefaultErrorStrategy.java:476)
	at org.antlr.v4.runtime.Parser.match(Parser.java:223)
	at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:165)
	at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:102)
	at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:221)
	at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:210)
	at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:72)
	at jkind.engines.KInductionEngine.checkProperties(KInductionEngine.java:88)
	at jkind.engines.KInductionEngine.main(KInductionEngine.java:53)
	at jkind.engines.Engine.run(Engine.java:36)
	at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
	at java.base/java.lang.Thread.run(Thread.java:832)
invariant-generation process failed
jkind.JKindException: Solver output parse error line 634:4 missing 'define-fun' at 'x!1'
	at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13)
	at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:67)
	at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:561)
	at org.antlr.v4.runtime.DefaultErrorStrategy.reportMissingToken(DefaultErrorStrategy.java:409)
	at org.antlr.v4.runtime.DefaultErrorStrategy.singleTokenInsertion(DefaultErrorStrategy.java:512)
	at org.antlr.v4.runtime.DefaultErrorStrategy.recoverInline(DefaultErrorStrategy.java:476)
	at org.antlr.v4.runtime.Parser.match(Parser.java:223)
	at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:165)
	at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:102)
	at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:221)
	at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:210)
	at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:72)
	at jkind.engines.invariant.AbstractInvariantGenerationEngine.refineBaseStep(AbstractInvariantGenerationEngine.java:74)
	at jkind.engines.invariant.AbstractInvariantGenerationEngine.main(AbstractInvariantGenerationEngine.java:49)
	at jkind.engines.Engine.run(Engine.java:36)
	at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
	at java.base/java.lang.Thread.run(Thread.java:832)

System info:

$ z3 --version
Z3 version 4.8.9 - 64 bit
$ git rev-parse HEAD # from inside the jkind repo
1f836bb08bc66256233fef4ee1a92e8c6a04592d
$ java --version
openjdk 14.0.2 2020-07-14
OpenJDK Runtime Environment (build 14.0.2+12)
OpenJDK 64-Bit Server VM (build 14.0.2+12, mixed mode)

The constrained output type in output variables with enum type

This file prompts:
Error at line 5: 72 function main may not use constrained output type (subrange or enumeration)
function main (choice: payload) returns (wolf, golds, cabbage, farmer: side);

Why it happens?
Some solutions please.

---

--farmer2.lus
type payload = enum { Empty, Wolf, Goat, Cabbage };
type side = enum { Left, Right };

function main(choice : payload) returns (wolf, goat, cabbage, farmer : side);

node testMain(choice : payload[2]) returns (wolf, goat, cabbage, farmer : side[2]);
var
wolf_0: side;
wolf_1: side;
golt_0: side;
golt_1: side;
cabbage_0: side;
cabbage_1: side;
farmer_0: side;
farmer_1: side;
let
wolf_0, golt_0, cabbage_0, farmer_0 = main(choice[0]);
wolf_1, golt_1, cabbage_1, farmer_1 = main(choice[1]);
wolf = [wolf_0, wolf_1];
goat = [goat_0, goat_1];
cabbage = [cabbage_0, cabbage_1];
farmer = [farmer_0, farmer_1];
tel;

Abnormal termination exit code -8 during IVC reduction

The problem occurs where IVC reduction appears to be attempted on a property that has (possibly) been falsified.

These errors occur intermittently but on some models more consistently than on others. Running the same model multiple times the error might or might not occur. When the error does not occur, the property(ies) in question is(are) valid. When it does occur, the property(ies) is(are) unknown. It appears to be some sort of race condition.

Initial analysis indicates that the errors do rarely occur in Java VM version 1.8 but occur much more frequently in later JVM versions.

Application of the same Lustre file to multiple versions indicates the errors may occur in (at least) JKind versions 4.4.4, 4.5.0, and 4.5.2.

The it seems that setting pdr_max to zero either eliminates the bug or makes it so much less probably that it was not detected in a few dozen runs.

I am struggling to put together a simple model that illustrates the problem; changing anything appears to affect the likelihood of occurrence.

JKind 4.4.3 - 4.4.4 has issues with Z3 4.8.11 and 4.8.12

This is not something we can fix and due to an underlying bug in Z3. Here is the related issue:

Z3Prover/z3#5599

Verbose output

Is there a verbose output option?

Confusions about the verification result

If there are too many variables and equations in Lustre program, some results confuse me.

1. The translation step prompts “OutOfMemoryError”. Monitoring tools show that the memory in old generation of JVM is full.
2. The solving step prompts “OutOfMemoryError”.
3. The solving step keep running without stop.
4. A relatively good result may be "Unknown Property" without some illustration to explain it. However, the same property in the same Lustre program appears "Valid" or "Invalid" after trying a computer with lager memory.

It will be inspiring if the above confusions can be improved.

(ps. Windows OS with 8G/16G/32G memory, solvers: smtinterpol, z3, mathsat, cvc (All are the latest release)).

Handle assertions and properties in subnodes

JKind should do something with assertions and properties in subnodes. There are different possible semantics for this, but one thing might be to just treat them all as proposed invariants.

Out of memory error on active-standby.kind.lus

I'm using jKind v2.1 from the binary releases and java 1.8.0_40 on Mac os x 10.9.5.
jKind crashes on the benchmark active-standby.kind.lus, it looks to be in the frontend because I'm trying to inspect jKind's dump files (in smtlib2 syntax, this is the only reason I use the flag -solver z3).

This is how I run it:

> jkind -scratch -no_inv_gen -no_k_induction -pdr_max 0 -n 0 -scratch -solver z3 active_standby.kind.lus

I get, after about 30s on my machine:

java.lang.OutOfMemoryError: Java heap space
    at java.util.Arrays.copyOf(Arrays.java:3181)
    at java.util.ArrayList.grow(ArrayList.java:261)
    at java.util.ArrayList.ensureExplicitCapacity(ArrayList.java:235)
    at java.util.ArrayList.ensureCapacityInternal(ArrayList.java:227)
    at java.util.ArrayList.add(ArrayList.java:458)
    at jkind.analysis.StaticAnalyzer.checkAlgebraicLoops(StaticAnalyzer.java:324)
    at jkind.analysis.StaticAnalyzer.checkAlgebraicLoops(StaticAnalyzer.java:331)
    ...

For info:

> java -XX:+PrintFlagsFinal -version | grep HeapSize
    uintx ErgoHeapSizeLimit                         = 0                                   {product}
    uintx HeapSizePerGCThread                       = 87241520                            {product}
    uintx InitialHeapSize                          := 134217728                           {product}
    uintx LargePageHeapSizeThreshold                = 134217728                           {product}
    uintx MaxHeapSize                              := 2147483648                          {product}
java version "1.8.0_40"
Java(TM) SE Runtime Environment (build 1.8.0_40-b25)
Java HotSpot(TM) 64-Bit Server VM (build 25.40-b25, mixed mode)

loop operation in Lustre

Loop operation is very important for program, especially for array operation.
However, if I am correct, Lustre language is applying cycle to array operation, instead of loop. Even the "normal" Lustre-v6 in Verimag is doing the same thing. I am confused with the feature in synchronous language.

For instance,

node main(in1: int[3]; in2: int[3])
returns(outp: bool; pArr: bool[3]);
var
out: bool;
let
out, pArr [0] = comput(in1[0], in2[0]);
out, pArr [1] = if out then comput(in1[1], in2[1]) else (false, false);
out, pArr [2] = if out then comput(in1[2], in2[2]) else (true, true);
outp = pArr[0] and pArr[1] and pArr[2];
--%PROPERTY outp;
tel;

node comput(arr1: int; arr2: int)
returns (result: bool; resultArr: bool);
let
resultArr = (arr1 > 0);
result = (arr2 > 0) and resultArr;
--%PROPERTY result;
tel;

The code prompts the "reassign" error.
So, any comments for my confusion?

Uncaught Exception

The IVC engine is crashing with the following error:

jkind.JKindException: Unable to find property event7_false_c4 during reduction
at jkind.engines.IvcReductionEngine.getInvariantByName(IvcReductionEngine.java:77)
at jkind.engines.IvcReductionEngine.reduce(IvcReductionEngine.java:65)
at jkind.engines.IvcReductionEngine.handleMessage(IvcReductionEngine.java:289)
at jkind.engines.messages.ValidMessage.accept(ValidMessage.java:43)
at jkind.engines.messages.MessageHandler.handleMessage(MessageHandler.java:31)
at jkind.engines.messages.MessageHandler.processMessagesAndWaitUntil(MessageHandler.java:39)
at jkind.engines.IvcReductionEngine.main(IvcReductionEngine.java:59)
at jkind.engines.Engine.run(Engine.java:35)
at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
at java.lang.Thread.run(Thread.java:748)

The lustre file to exercise the error is attached as a text file.

bug.txt

Differentiate unknown results

It would be nice if JKind would differentiate between different kinds of unknown results: max iterations, timeout, or other failure.

Additional static checks

JKind should be able to check for unguarded pre expressions and for algebraic loops. However, perhaps they should only be warnings since we can still make sense of such Lustre programs in JKind. Additionally, one of our tools at Rockwell (purposefully) generates Lustre code with algebraic loops in some circumstances.