Context Navigation

README @ 11

Last change on this file since 11 was 11, checked in by cecile, 13 years ago
Add vis
File size: 667 bytes

Line
1	read_blif_mv crd.mv
2	init
3	mc crd_rs.ctl
4	#we are just checking for reachability
5	mc lang_empt.ctl
6	# the language should not be empty at this stage.
7	read_fairness crd.fair
8	mc lang_empt.ctl
9	# it should still not be empty
10	mc starvation.ctl
11	#should pass
12	mc starvation2.ctl
13	#should pass. this just uses monitor "starvation" instead of at the root.
14	#in hsis we did this with fairness constraints on starvation, but we
15	# cannot express these with Buchi conditions (same as in ping_pong.
16	mc safety.ctl
17	#this should pass
18	read_fairness safety.fair
19	# we have put fairness constraints on the monitor "collision"
20	mc lang_empt.ctl
21	#this should pass since we only accept bad behavior.

Note: See TracBrowser for help on using the repository browser.