Rev | Line | |
---|
[11] | 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.