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