Context Navigation

check_script @ 14

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

Line
1	read_blif_mv ping_pong.mv
2	init_verify
3	compute_reach -v 1
4	print_fairness
5	lang_empty -d 0
6	# reachable # states is 5
7	read_fairness prop1.fair
8	print_fairness
9	lang_empty -d 0
10	#this should pass
11	read_fairness ping_pong.fair
12	print_fairness
13	lang_empty -d 0
14	#this should fail
15	model_check -d 0 prop2.ctl
16	#this should pass
17	model_check -d 0 ping_pong.ctl
18	# Both formulas should pass
19	# now flush the fairness constraints.
20	reset_fairness
21	print_fairness
22	model_check -d 0 ping_pong.ctl
23	#The first one should pass and the last should fail
24	time
25	quit -s

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