kind2-mc / kind2 Goto Github PK
View Code? Open in Web Editor NEWMulti-engine SMT-based automatic model checker for safety properties of Lustre programs
Home Page: https://kind.cs.uiowa.edu
License: Apache License 2.0
Multi-engine SMT-based automatic model checker for safety properties of Lustre programs
Home Page: https://kind.cs.uiowa.edu
License: Apache License 2.0
Techniques failing do not cause the analysis to stop but, in XML output, each failure emits the AnalysisStop
tag and closes Result
.
node blah(in_1, in_2: real) returns (out: real) ;
var mul: real ;
let
mul = in_1 * in_2 ;
out = if mul < 0.0 then - mul else mul ;
--%PROPERTY out >= 0.0 ;
tel
<?xml version="1.0"?>
<Results xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" enabled="bmc,ind,ind2,ic3,invgents,invgenos" timeout="0.000000" bmc_max="0" compositional="false" modular="false">
<Log class="info" source="parse">kind2 v1.0.alpha1-24-g8c260b8</Log>
<AnalysisStart top="blah" concrete="blah" abstract="" assumptions=""/>
<Log class="error" source="ic3">In property directed reachability: a check-sat resulted in "unknown", exiting.</Log>
<AnalysisStop/>
</Results>
<Log class="error" source="invgenos">In one state invariant generator: a check-sat resulted in "unknown", exiting.</Log>
<Log class="error" source="invgents">In two state invariant generator: a check-sat resulted in "unknown", exiting.</Log>
<AnalysisStop/>
</Results>
<AnalysisStop/>
</Results>
<Property name="(out >= 0.0)"><Runtime unit="sec" timeout="false">0.068</Runtime><Answer source="ind">valid</Answer></Property>
<AnalysisStop/>
</Results>
Hi Daniel,
Using the last version of Kind2 in develop branch I get this error very often today.
kind2 v1.1.0-283-g270c506c
Runtime error in invariant manager: Not_found
Do you know what may cause it?
Thanks
Running this file with Kind 2 produces an error about PDR and reals:
<?xml version="1.0"?>
<Results xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
<Log class="info" source="parser">kind2 v0.1.1-440-gbab8e9d</Log>
<Log class="fatal" source="invman">
Runtime error: Failure("Non-integer terms not supported. Use a different --pdr_qe option.")
</Log>
<Log class="fatal" source="invman">
Runtime error: Failure("Non-integer terms not supported. Use a different --pdr_qe option.")
</Log>
<Log class="error" source="invman">
Child process 23682 (PDR) exited with return code 2
</Log>
<Property name="_SYS_GUARANTEE_1">
<Answer>unknown</Answer>
<TrueFor>3</TrueFor>
</Property>
<Property name="_SYS_GUARANTEE_0">
<Answer>unknown</Answer>
<TrueFor>3</TrueFor>
</Property>
</Results>
Kind 2 sometimes produces error messages for this file:
node top (init: int) returns (OK: bool);
var
V4_time: int;
let
OK = (V4_time < 0);
V4_time = (0 -> (if ((pre V4_time) = 5) then 0 else ((pre V4_time) + 1)));
--%PROPERTY OK;
tel;
I get the following output (sometimes):
kind2 v0.7.0
Failure: Property OK is invalid for k=0 by BMC
Counterexample for OK:
Node top ()
init 0
OK false
V4_time 0
Child process 7643 (PDR) exited with return code 2
Runtime error: File "PDR.ml", line 1621, characters 22-28: Assertion failed
Runtime error: File "PDR.ml", line 1621, characters 22-28: Assertion failed
When Kind2 cannot determine the validity of a property, I would expect the following in the XML file:
<Property name="prop1">
<Answer>unknown</Answer>
</Property>
Instead, there is Property
tag for prop1. Instead you would have to read through the property summaries:
<property name="prop1"><status>true(12)</status></property>
Is it possible to include an actual Property
tag for unknown properties.
Summarizing this with previous requests, I expect the XML file to have exactly one Property
tag for each property I give to kind2 (which is either valid, falsifiable, or unknown).
In the latest version on develop branch there is no file flags.ml.in
See this post.
The constraints we introduce on function
s (as opposed to node
s) trigger the theory of uninterpreted functions at SMT-level. When the functions are fully-defined, this constraint is perfectly useless as the stream definitions alone guarantee that the functions yields the same outputs when given the same inputs.
We should check whether all outputs appear on the lhs of a lustre declaration in functions to decide whether we add the constraints triggering UFs or not. That way, users could still use function
s without the additional cost at SMT-level, but with the checks we do on the absence of temporal operators.
NB: looking at the outputs only as opposed to the outputs and all local variables in their coi
is enough because, currently, local variables cannot be undefined.
If this changes, then the solution proposed here is not enough.
Currently negative numbers are printed in a sexp format in the XML output:
<stream name="z" type="int" class="output">
<value state="0">1</value>
<value state="1">(- 1)</value>
<value state="2">(- 1)</value>
</stream>
I would prefer just
<stream name="z" type="int" class="output">
<value state="0">1</value>
<value state="1">-1</value>
<value state="2">-1</value>
</stream>
The same goes for reals which are printed as
<stream name="r" type="real" class="input">
<value state="0">(/ 1.0 2.0)</value>
<value state="1">(/ 1.0 2.0)</value>
<value state="2">(/ 1.0 2.0)</value>
</stream>
I would prefer just
<stream name="r" type="real" class="input">
<value state="0">1/2</value>
<value state="1">1/2</value>
<value state="2">1/2</value>
</stream>
That is, removing both the sexp format and not using decimal points.
Running this file in kind2 produces:
<?xml version="1.0"?>
<Results xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance">
<Log class="info" source="parser">kind2 v0.1.1-440-gbab8e9d</Log>
<Property name="_SYS_GUARANTEE_1">
<Runtime unit="sec" timeout="false">0.437</Runtime>
<K>1</K>
<Answer source="bmc">falsifiable</Answer>
<Counterexample>
<Log class="fatal" source="invman">Runtime error: Not_found</Log>
<Property name="_SYS_GUARANTEE_8"><Answer>unknown</Answer></Property>
<Property name="_SYS_GUARANTEE_7"><Answer>unknown</Answer></Property>
<Property name="_SYS_GUARANTEE_6"><Answer>unknown</Answer></Property>
<Property name="_SYS_GUARANTEE_5"><Answer>unknown</Answer></Property>
<Property name="_SYS_GUARANTEE_4"><Answer>unknown</Answer></Property>
<Property name="_SYS_GUARANTEE_3">
<Answer>unknown</Answer>
<TrueFor>0</TrueFor>
</Property>
<Property name="_SYS_GUARANTEE_2"><Answer>unknown</Answer></Property>
<Property name="_SYS_GUARANTEE_1"><Answer>unknown</Answer></Property>
<Property name="_SYS_GUARANTEE_0"><Answer>unknown</Answer></Property>
</Results>```
Hi,
I'm a bit confused by the behaviour of "assert". I expected it to act more like "assume", in that it would be assumed to be true while verifying the node containing the assertion, but would be required to be shown to be true wherever the node is used. At the moment, it seems to assume it to be true in both cases. The documentation doesn't really explain assert, so I don't know whether this is me not understanding the purpose of assert, or a bug in assert.
Here is a concrete example:
node weird_plus(a, b : int) returns (o : int)
let
assert a = b;
o = a * 2;
--%PROPERTY o = a + b;
tel
node should_fail(a, b : int) returns (o : int)
/*@contract
assume a <> b;
guarantee o = a + b;
*/
let
o = weird_plus(a, b);
tel
Node weird_plus
asserts that both inputs are equal and adds them together by doubling one of the inputs. This property succeeds, as expected.
Then, the node should_fail
assumes that the two inputs are different, and tries to use weird_plus
to add them together. I expected this use of weird_plus
to fail because weird_plus
has the precondition that a = b
, which is not true here. However, the property succeeds.
Is this the expected behaviour?
Thanks,
Amos
It looks like subrange information on inputs is being ignored. For example, the following property fails:
node main (in : subrange [0, 1] of int) returns (ok : bool);
let
ok = 0 <= in and in <= 1;
--%PROPERTY ok;
tel;
When I use option timeout_analysis I get the following error.
Fatal error: exception Unix.Unix_error(Unix.ENOENT, "stat", "\194\150")
Hi Daniel,
It seems that the order of nodes is important for contracts, any node used by a contract should be declared before it in the lustre file.
Example:
`
node mod_real(x, y: real;)
returns( z: real );
(*@contract
guarantee abs_real(z) < abs_real(y);
*)
let
tel
node abs_real (x: real)
returns(y:real);
let
y= if x >= 0.0 then x
else -x;
tel
`
Kind2 error: unknown node or function "abs_real"
Source: parse
Is it possible to fix this in Kind2, or it's for implementation reasons we can not?
Thanks,
Hamza
Hi Daniel,
I have an issue building Kind2. Maybe because we have different C compilers.
Attached is the log file that may help you understand the error.
I think it's an issue of a buffer size that should be increased.
For the AGREE tool we are generating Lustre with nested records. Based on kind2 outout and browsing the Lustre grammar, it looks like kind2 does not yet supported nested record access. For example, the following file generates a parser error:
type point = struct { x : int; y : int };
type weighted_point = struct { weight : real; p : point };
node main(wp : weighted_point) returns (sum : int);
let
sum = wp.p.x + wp.p.y;
tel;
Yields
Parser error in line 6 col. 12: Syntax error
I noticed that contract ghost vars are limited to one var per statement:
var v:v_type = e;
How we can declare more than one var for the same expression?
var (v1,v2) :(t1, t2)= f(); where f could be a function/node with two outputs.
Is it not currently supported by Kind2?
Hi Daniel,
How we can define a stream that is clocked in Kind2 syntax?
As it seems from the following code, Kind2 asking me to use the "current" operator when I use "when". In Lustre, we can define streams that are clocked by some bool clock.
node _make_clock(per: int; ph: int)
returns( clk: bool );
var cnt: int;
let
cnt = ((per - ph) -> (pre(cnt) + 1)) mod per ;
clk = if (cnt = 0) then true else false ;
tel
node trigger_test_PP(In1_1 : real;)
returns(Out1_1 : real;);
var RateTransition_1 : real;
RateTransition1_1 : real;
__time_step : real;
_clk_2_0 : bool ;
let
RateTransition_1 = (In1_1 when _clk_2_0);
RateTransition1_1 = (merge _clk_2_0
(true -> (0.000000000000000 -> (pre RateTransition_1)))
(false -> ((0.000000000000000 -> (pre RateTransition1_1)) when not(_clk_2_0))));
Out1_1 = RateTransition1_1;
__time_step = (0.0 -> ((pre __time_step) + 1.000000000000000));
_clk_2_0 = _make_clock(2, 0);
tel
Thanks,
Hamza
Hi,
I am trying to use compositional verification on the attached example. I tried garantee and mode version. I keep getting " Illegal unguarded pre under a node call in this contract" error
where I can not trace and understand.
Thanks in advance
Hamza
two_counters.txt
For some reason (nested configure scripts or such), the configure script
outputs an error message, but does not fail after AC_MSG_ERROR
. Need
to investigate more.
Seems that some case is missing:
diff --git a/src/simplify.ml b/src/simplify.ml
index 6f2e73ec..fc43b180 100644
--- a/src/simplify.ml
+++ b/src/simplify.ml
@@ -1909,6 +1909,8 @@ let rec simplify_term_node default_of_var uf_defs model fterm args =
(* New polynomial with integer value as atom *)
Dec (Decimal.zero, [Decimal.one, [Term.mk_to_int (term_of_nf a)]])
+ | [Dec _ as a] -> a
+
(* Conversion is only unary *)
| _ -> assert false
==> ./autogen.sh
autoreconf: Entering directory .' autoreconf: configure.ac: not using Gettext autoreconf: running: /opt/local/bin/aclocal -I config --force -I config autoreconf: configure.ac: tracing autoreconf: configure.ac: not using Libtool autoreconf: running: /opt/local/bin/autoconf --include=config --force configure.ac:52: error: missing some pkg-config macros (pkg-config package) If this token and others are legitimate, please use m4_pattern_allow. See the Autoconf documentation. configure.ac:61: error: possibly undefined macro: AC_LIBTOOL_WIN32_DLL configure.ac:62: error: possibly undefined macro: AC_PROG_LIBTOOL configure.ac:426: error: missing some pkg-config macros (pkg-config package) configure:5403: error: possibly undefined macro: AC_DISABLE_STATIC configure:5407: error: possibly undefined macro: AC_ENABLE_STATIC autoreconf: /opt/local/bin/autoconf failed with exit status: 1 autogen.sh: error: autoreconf exited with status 0 ./autogen.sh: line 10: pushd: czmq: No such file or directory autoreconf: Entering directory
.'
autoreconf: configure.ac: not using Gettext
autoreconf: running: /opt/local/bin/aclocal -I config
autoreconf: configure.ac: tracing
autoreconf: configure.ac: not using Libtool
autoreconf: running: /opt/local/bin/autoconf
configure.ac:52: error: missing some pkg-config macros (pkg-config package)
If this token and others are legitimate, please use m4_pattern_allow.
See the Autoconf documentation.
configure.ac:61: error: possibly undefined macro: AC_LIBTOOL_WIN32_DLL
configure.ac:62: error: possibly undefined macro: AC_PROG_LIBTOOL
configure.ac:426: error: missing some pkg-config macros (pkg-config package)
configure:5403: error: possibly undefined macro: AC_DISABLE_STATIC
configure:5407: error: possibly undefined macro: AC_ENABLE_STATIC
autoreconf: /opt/local/bin/autoconf failed with exit status: 1
autoreconf: Entering directory .' autoreconf: configure.ac: not using Gettext autoreconf: running: /opt/local/bin/aclocal autoreconf: configure.ac: tracing autoreconf: configure.ac: adding subdirectory libzmq to autoreconf autoreconf: Entering directory
libzmq'
autoreconf: running: /opt/local/bin/aclocal -I config
autoreconf: configure.ac: not using Libtool
autoreconf: running: /opt/local/bin/autoconf
autoreconf: running: /opt/local/bin/autoheader
autoreconf: running: /opt/local/bin/automake --no-force
configure.ac:46: error: required file 'config/compile' not found
configure.ac:46: 'automake --add-missing' can install 'compile'
configure.ac:60: error: required file 'config/config.guess' not found
configure.ac:60: 'automake --add-missing' can install 'config.guess'
configure.ac:60: error: required file 'config/config.sub' not found
configure.ac:60: 'automake --add-missing' can install 'config.sub'
configure.ac:14: error: required file 'config/install-sh' not found
configure.ac:14: 'automake --add-missing' can install 'install-sh'
configure.ac:14: error: required file 'config/missing' not found
configure.ac:14: 'automake --add-missing' can install 'missing'
Makefile.am:16: error: Libtool library used but 'LIBTOOL' is undefined
Makefile.am:16: The usual way to define 'LIBTOOL' is to add 'LT_INIT'
Makefile.am:16: to 'configure.ac' and run 'aclocal' and 'autoconf' again.
Makefile.am:16: If 'LT_INIT' is in 'configure.ac', make sure
Makefile.am:16: its definition is in aclocal's search path.
Makefile.am: error: required file 'config/depcomp' not found
Makefile.am: 'automake --add-missing' can install 'depcomp'
parallel-tests: error: required file 'config/test-driver' not found
parallel-tests: 'automake --add-missing' can install 'test-driver'
autoreconf: /opt/local/bin/automake failed with exit status: 1
Hello,
is there a possibility to express the (square) root operator in Kind2 so that SMT-Solvers get along with it? I tried implementing the square root operator using Heron algorithm with inductive array defintion and old fashioned simple variables. But SMT-Solvers do not get along with that. As far as i know Z3 supports root operators. Am i missing a operator for square root or is that not part of Kind2 like it is in Lustre?
Thanks for help.
The downloads for kind2 are .tar.gz
files but are actually just in the tar format. This can cause tar
to fail to unpack them correctly.
Hi Daniel,
I face this error using docker on Centos 6.9
docker run -v /data/software/cocoTeam/demo2/models_with_properties/lustre_files/src_tcm_with_properties_PP:/lus kind2/kind2:dev -xml --timeout 60.0 --lus_main tcm_with_properties_PP_TCM_Longitudinal_Guide_130 /lus/tcm_with_properties_PP.lus
kind2 v1.1.0
Error opening input file "/lus/tcm_with_properties_PP.lus":
Sys_error("/lus/tcm_with_properties_PP.lus: No such file or directory")
Normally the file tcm_with_properties_PP.lus does exist in /data/software/cocoTeam/demo2/models_with_properties/lustre_files/src_tcm_with_properties_PP repo
Do you have any idea?
Thanks
Hamza
When I run this file I get
<log class="error" source="invman">
Child process 28987 (PDR) exited with return code 2
</log>
Hi Daniel,
I know there is a possibility to do a Bottom-up analysis of each node (using --modular true).
What about a top-down analysis in a compositional setting. I believe it may produce results for top contracts in the limited timeout given by the user for large complex models. While most of the time in bottom-up analysis, I noticed kind2 gives up quickly on the bottom contracts as they are hard to prove and it stops the analysis.
top-down analysis may require computing the dependency graph of nodes and do a BFS of contracts.
--timeout_analysis is useful to limit the timeout per analysis, but I would like to experiment kind2 in a top-down analysis.
In the mean time, what about an option to give a list of nodes to analyze by order in the same execution? Currently I use --lus_main for each node on several executions of kind2.
Thanks
Subrange checking does not handle if-then-else and arrow. Consider:
node main(b : bool) returns ();
var
x1 : subrange [0, 1] of int;
x2 : subrange [0, 1] of int;
let
x1 = if b then 0 else 1;
x2 = 0 -> 1;
tel;
This gives:
Parser warning in line 6 col. 2: Cannot determine correctness of subrange type, adding constraint as property.
Parser warning in line 7 col. 2: Cannot determine correctness of subrange type, adding constraint as property.
I would expect kind2 to be able to statically confirm the correctness of these subrange types.
In ./configure I get this error:
configure: error: cannot find install-sh, install.sh, or shtool in "." "./.." "./../.."
Kind 2 does not allow forward references such as in these examples:
type t1 = struct { x : t2 };
type t2 = int;
const c1 = c2;
const c2 = 1;
node main() returns (ok : bool);
let
ok = other();
tel;
node other() returns (ok : bool);
let
ok = true;
tel;
From this Lustre manual:
Four kinds of objects can be declared: [Constants, Types, Functions, Nodes]. The order of these declarations is meaningless. All the declared objects are global to the program. (Page 15)
Types can be declared in any order. (Page 24)
Constants can be declared in any order. (Page 30)
Nodes can be declared in any order. (Page 35)
Moreover, when generating Lustre files it is often inconvenient to have to topologically sort all types, constants, and nodes. It would be great if Kind 2 could be extended to allow arbitrary order of definitions.
Hi
I have a problem in another machin I am testing in ubuntu 14.4.
please find the log attached when running ./build.sh
log.txt
Sometimes the XML output is buggy. For example running this
kind2 AltitudeControl_Demo.lus --z3_bin z3 --lus_main AltitudeControl_Demo_SAFETY_REQUIREMENT_2 -xml
on the following file
sometimes it gives a mal-formed xml file:
I'm using the file 8peg.lus and running kind2 (over the web interface) with arguments:
-xml --timeout_wall 5
And it looks like kind2 reports my property as unknown
after 5 seconds, but then it continues to run for a long time afterwards before the final </Results>
tag is shown.
Hi,
I used the stopwatch example from the Kind2 web interface. I modified the code in order to remove the implementation of node stopWatch and use explicit traces instead. Please find the code attached: test2.txt
The stopwatchSpec has only one assumption
assume not (toggle and reset) ;
and I have added these two assertions in the stopwatch node:
assert toggle = true -> pre( false -> pre(false -> false));
assert reset = false -> pre( false -> pre(true -> false));
I get always the following error: 'BMC Unrolling of the system is unsat at 1, the system has no more reachable states.'. Does this mean that my assumptions are inconsistent?
Could you please help me figure out what the problem is?
Running Ubuntu 16.04 with OCaml 4.04. The system OCaml compiler is 4.02.3 (i.e., for each new terminal, ocaml -version
returns "4.02.3"), but I switched compilers to 4.04 via opam switch 4.04.0
and set the environment accordingly (i.e., ocaml -version
returns 4.04.0).
Have installed everything listed here:
https://kind.cs.uiowa.edu/kind2_user_doc/home.html#requirements
autogen.sh seems to run fine, but when I run ./build.sh
(I'm fine with default directory), it terminates with the following:
+ /usr/bin/ocamlopt -c -w @P@U@F -I /home/local_user/.opam/4.04.0/lib/biniou -I /home/local_user/.opam/4.04.0/lib/easy-format -I /home/local_user/.opam/4.04.0/lib/yojson -annot -bin-annot -I utils -I c2i -I invgen -I qe -I lustre -I ic3 -I certif -I doc -I smt -I terms -I testgen -I induction -o utils/hString.cmx utils/hString.ml
File "utils/hString.ml", line 224, characters 14-36:
Error: Unbound value String.uppercase_ascii
Command exited with code 2.
Makefile:8: recipe for target 'kind2' failed
make[1]: Leaving directory '/home/local_user/kind2gh/src'
Makefile:39: recipe for target 'kind2' failed
See log attached.
log.txt
Module Event
seems to conflict with recent ocaml versions (at least 4.05):
Error: Files event.cmx and /usr/local/lib/ocaml/threads/threads.cmxa
both define a module named Event
The compilation fails because Ocaml does not anymore treat bytes and string the same. The error message is:
/home/ayrat/.opam/4.07.0/bin/ocamlopt.opt -c -w @P@U@F -annot -bin-annot -thread -color always -I utils -I testgen -I invgen -I induction -I ic3 -I qe -I smt -I c2i -I terms -I certif -I lustre -I doc -o utils/lib.cmx utils/lib.ml
File "utils/lib.ml", line 1:
Error: The implementation utils/lib.ml
does not match the interface utils/lib.cmi:
Values do not match:
val string_starts_with : bytes -> bytes -> bool
is not included in
val string_starts_with : string -> string -> bool
File "utils/lib.mli", line 64, characters 0-49: Expected declaration
File "utils/lib.ml", line 583, characters 4-22: Actual declaration
More details from ocaml docs:
The distinction between bytes and string was introduced in OCaml 4.02, and the "unsafe-string" compatibility mode was the default until OCaml 4.05. Starting with 4.06, the compatibility mode is opt-in; we intend to remove the option in the future.
Given the following:
function imported imp(x: int) returns (y: int);
function min(x,y:int) returns (z: int)
(*@contract
assume true;
*)
let
z = if x < y then x else y;
tel
function main(x:int) returns (y:int)
let
y = min(imp(2),10);
--%PROPERTY y <= 10;
tel
Running kind2 with --compositional true --modular true
, it fails to prove the (obviously correct) property of main
because it does not attempt to refine min
, seemingly due to the presence of abstract imp
.
Either removing min
’s contract, or giving imp
a concrete implementation, causes kind2 to verify the property as expected.
This behavior seems to be somewhat order-dependent. For example, replacing:
y = min(imp(2),10);
with
y = foo(min(2,10));
does result in refinement of min
, though of course the property does not verify since it’s false.
kind2 nightly-68-g48a0a6fd
The develop branch fails to build on Debian sid because of the use of the deprecated macro _BSD_SOURCE in czmq:
In file included from /usr/include/ctype.h:25:0,
from ../include/czmq_prelude.h:203,
from ../include/czmq.h:19,
from zauth.c:25:
/usr/include/features.h:148:3: error: #warning "_BSD_SOURCE and _SVID_SOURCE are deprecated, use _DEFAULT_SOURCE" [-Werror=cpp]
# warning "_BSD_SOURCE and _SVID_SOURCE are deprecated, use _DEFAULT_SOURCE"
^
cc1: all warnings being treated as errors
This has been fixed upstream in czmq so it's just a matter of updating.
In addition to submitjob
, retrievejob
, canceljob
, it would be nice if there were a URL or service to invoke to check that a kind2 webserver is up and running at the given URL. For example, the user inputs localhost:1234
and I can check localhost:1234/status
or localhost:1234/test
or whatever to see that the user's URL is good.
Hello,
I am learning on the course Formal Software Verification. This week is about model checking and one of the tasks suggests me to use a tool of my own choice to prove if the following code is valid or not. I am wondering if I could accomplish this task with kind2.
I have installed the Docker image and can run the example I got from doc/usr/content/2_input. However, the tutorials are not enough for me to understand the following:
Set beam = B
is called?setBeam
and setPlate
are executed (to ensure all combinations of states/plates are covered)?OK =
value which should be equal to not (plate = 2 and beam 2)
?P.S. I am very new to model checking. Still, I hope I am not asking something completely dumb and simple.
Thanks.
I am building a cancer treatment machine. The machine can emit two types of beams; for simplicity let’s just call them A and B. There are two different plates that can be placed in front of the beam; let’s call them 1 and 2. When you turn the machine on it always starts ups with beam set to A and plate set to 1. That is the initial state.
For safety reasons we never want the machine to be at beam B and plate 2. If this every happens a deadline dose of radiation will be emitted and it will kill the patient. But all of the other combinations of beams and plates are valid.
I have a developer write code to automate this machine. He claims that his software will prevent the machine from ever being in state beam = A and plate = 2.
Here is his code. Use Model Checking to software this problem.
Method setBeam(str beamType)
If beamType = B and plate = 1
Set beam = B
Else Set beam = A
Method setPlate(int plateType)
If plateType = 2 and beam = A
Set plate = 2
Else Set plate = 1
Is he correct?
The bug happens when a node has a constant input and passes it through a call to a subnode accepting non-constant inputs.
node count (in: bool) returns (cnt: int) ;
let
cnt = (if in then 1 else 0) + (0 -> pre cnt) ;
tel
node top (const in: bool) returns (cnt: int) ;
(*@contract
guarantee cnt >= 0 ;
*)
let
cnt = count(in) ;
tel
The actual problem is an arity mismatch at SMT-level between the signature of the subnode and the way the caller uses it. That's because the constant state variable is only passed once since it's constant, where as the subnodes expects to see the previous and current versions.
The following program is accepted but it is ill-typed.
const w = 11;
const n = 5;
node f(x : bool) returns (b : bool^n);
let
b = false ^ n;
tel
node b(x : bool)
returns (xb : bool^w);
let
--%PROPERTY xb[1] = false;
xb = f(x);
tel
Issue originally reported here:
If I have a node with contract inclusion but I forget to include the file containing the contract I have a strange message about Circular dependency in contract. For example:
-- include "spec.lus" let comment it
node X...;
(*@contract
import C;
*)
kind2 ...
<Error> Parser error at line 64 col. 0: Circular dependency in contract :
import C (
...
) (...) ;
Maybe it's better to tell the user that the imported contract is not defined.
Hi Daniel,
Attached is the example of a lustre code contains an automaton.
I run the command
kind2 -xml test3.lus --enable interpreter --timeout 60
I get the following error
<Stream
name="state" <Log class="fatal" source="parse">
Runtime error in interpreter: File "lustre/lustrePath.ml", line 1243, characters 18-24: Assertion failed
</Log>
I am only interested to check if the lustre code is correct syntactically.
Do you know of another option rather than the one I used to check a Lustre file is accepted by Kind2?
If not, is the above error can be easily fixed from your side?
Thanks,
Hamza
test3.txt
Hi Daniel,
Is it normal That Kind2 gives different result for different executions, It gives me Unknown and sometimes a Counter Example.
I know that it depends on which solver it uses, so in case if we don't fix the solver, is it not deterministic?
PS: I am using the docker version, I tried also to rebuild it from the last version of kind2 in develop branch.
Thanks
Hamza
Hi Daniel
I got this error runing : docker build -t kind2-local .
Step 30/41 : RUN ./latest_proof_cvc4.sh
---> Running in 764db9b71eb1
--2017-04-18 00:29:15-- http://cvc4.cs.nyu.edu/cvc4-builds/x86_64-linux-opt-proofs/unstable/
Resolving cvc4.cs.nyu.edu (cvc4.cs.nyu.edu)... 128.122.49.30
Connecting to cvc4.cs.nyu.edu (cvc4.cs.nyu.edu)|128.122.49.30|:80... connected.
HTTP request sent, awaiting response... 302 Found
Location: http://cvc4.cs.stanford.edu/ [following]
--2017-04-18 00:29:16-- http://cvc4.cs.stanford.edu/
Resolving cvc4.cs.stanford.edu (cvc4.cs.stanford.edu)... 171.64.78.10
Connecting to cvc4.cs.stanford.edu (cvc4.cs.stanford.edu)|171.64.78.10|:80... connected.
HTTP request sent, awaiting response... 301 Moved Permanently
Location: http://cvc4.cs.stanford.edu/web/ [following]
--2017-04-18 00:29:17-- http://cvc4.cs.stanford.edu/web/
Reusing existing connection to cvc4.cs.stanford.edu:80.
HTTP request sent, awaiting response... 200 OK
Length: unspecified [text/html]
Saving to: 'index'
0K .......... .......... .... 244K=0.1s
2017-04-18 00:29:17 (244 KB/s) - 'index' saved [24647]
could not retrieve latest cvc4 version
The command '/bin/sh -c ./latest_proof_cvc4.sh' returned a non-zero code: 2
Kind 2 treats the the declaration int^3^2
as an array of size 3 each of whose elements are arrays of size 2. This is backwards from Lustre and SCADE.
cf. Scade Language Primer, Section 5.3, Multidimensional Operators:
Array types are unidimensional: it is not possible in Scade to directly define
multidimensional arrays. A matrix is encoded by an array of arrays, as in:
type SpaceLinearMorphism = real ^ 4 ^ 6 ;
mat : SpaceLinearMorphism ;
This defines a matrix of six arrays of four elements each. Selecting an element in this array
by the expressionmat[i][j]
first checks whetheri
belongs to interval[0..5]
then thatj
belongs to[0..3]
. Notice the order of index declaration is the reverse from the
one used for selection.
Hi,
I get the following error while running make install
:
[root@3f1f0dc2e19a kind2]# make install
mkdir -p /root/install/kind2/bin
for i in kind2 lfsc-extractor cvc4_lfsc_check; do \
install -m 0755 /root/build/kind2/bin/$i /root/install/kind2/bin/$i; \
done
install: cannot stat `/root/build/kind2/bin/lfsc-extractor': No such file or directory
install: cannot stat `/root/build/kind2/bin/cvc4_lfsc_check': No such file or directory
I just looked at the Makefile.in
. I guess lfsc_extractor
and cvc4_lfsc_check
are optional, and thus make install
shouldn't fail if they are missing.
We add each property as an output, but this fails with a duplicate variable declaration if the property is an input. Before adding a property as an output, check if the property is an input and make a copy of the input stream to be output.
Example:
node X (OK: bool) returns ();
let
--%PROPERTY OK;
tel
For the following Lustre program, Kind 2 reports a counterexample of length 4, but I believe the minimal counterexample length is 12.
node pass(x : int) returns (y : int);
let
y = 0 -> pre x;
tel;
node main() returns ();
var
count : int;
toggle : bool;
ok : bool;
slow_count : int;
let
count = 3 -> 1 + pre count;
toggle = false -> not pre toggle;
slow_count = condact(toggle, pass(count), -1);
ok = slow_count <= 10;
--%PROPERTY ok;
tel;
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.