You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
30 lines
858 B
30 lines
858 B
|
|
|
|
TODO:
|
|
|
|
new version of valid2 (inv/g push outside)
|
|
|
|
combined complement + intersection (terminating early) for when dbm lists get big
|
|
|
|
----------------------
|
|
|
|
BUGS:
|
|
|
|
----------------------
|
|
----------------------
|
|
|
|
./forwardreach examples/repudiation/originator.des examples/repudiation/recipient.des examples/repudiation/honest_deadline40.des '*:*:before' 'true' -min -opt -nopre
|
|
Final TPSG: 416 states, 1813 distribution sets, 2221 distributions, 3751 transitions, p1max/avg = 3/4.4, p2max/avg = 2/1.2
|
|
(avg > max)
|
|
|
|
----------------------
|
|
|
|
Questions:
|
|
|
|
is it safe to split (refine) multiple states concurrently in the way that we do?
|
|
|
|
do we want to check for duplicate sym states when creating new ones through refinement?
|
|
- is this safe?
|
|
|
|
are we ok to have non-diagonal c-closure algorithm?
|
|
or is it ok if only use this on initial reach graph construction?
|