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

3 commits

Author SHA1 Message Date
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