alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
2007 commits 6 branches 0 tags 36 MiB
Commit graph

6 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
40de47f159 dve2: use postprocessor to simplify the code. 
* iface/dve2/dve2check.cc: Use postprocessor to simplify the code.
* iface/dve2/dve2check.test: Adjust to some different output values
when a counterexample is found, caused by nondeterminism introduced by
the orders of transitions.
 2012-09-21 15:10:13 +02:00
Alexandre Duret-Lutz
03aca91648 Don't compare memory consumption between 2 runs of dve2check 
* iface/dve2/dve2check.test: Here.
 2012-04-27 22:47:54 +02:00
Alexandre Duret-Lutz
1719287b1e -e means we expect an accepting run. 
* iface/dve2/dve2check.cc: Reverse the value of
expect_counter_example with respect to the -e/-E options.
* iface/dve2/dve2check.test: Swap -e and -E.
 2011-07-26 18:44:18 +02:00
Alexandre Duret-Lutz
c938e652e4 DVE2: preliminary implementation of compressed states. 
* iface/dve2/dve2.cc (dve2_compressed_state): New class.
(callback_context): Deal with general state*s, not dve2_state*s.
(transition_callback_compress): New function.
(dve2_kripke): Take a compress option.
(get_init_state, compute_state_condition, succ_iter,
format_state, state_condition): Handle compressed states.
(get_vars, compute_state_condition_aux): New helper methods.
* iface/dve2/dve2.hh (load_dve2): Add a compress option.
* iface/dve2/dve2check.cc: Add a -z option.
* iface/dve2/finite.test, iface/dve2/dve2check.test: Add more
tests.
 2011-04-09 17:34:04 +02:00
Alexandre Duret-Lutz
8256ae9bfb Accept "P_0 == CS" as synonym for "P_0.CS" in the dve2 interface. 
Suggested by Yann Thierry-Mieg.

* iface/dve2/dve2.cc (convert_aps): Allow string on the right
of operators, and look them up.
* iface/dve2/dve2check.test: Test this syntax.
 2011-03-07 12:45:37 +01:00
Alexandre Duret-Lutz
5318c1f966 Add some tests for the DVE2 interface. 
* iface/dve2/defs.in, iface/dve2/dve2check.test,
iface/dve2/beem-peterson.4.dve: New files.
* iface/dve2/Makefile.am: Add them.
* configure.ac: Generate iface/dve2/defs.
 2011-03-07 12:24:32 +01:00