| changeset 5313 | 1861a564d7e2 |
| parent 5277 | e4297d03e5d2 |
| child 5648 | fe887910e32e |
| 5312:b380921982b9 | 5313:1861a564d7e2 |
|---|---|
8 The state is identified with the one variable in existence. |
8 The state is identified with the one variable in existence. |
9 |
9 |
10 From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1. |
10 From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1. |
11 *) |
11 *) |
12 |
12 |
13 Common = WFair + Traces + |
13 Common = SubstAx + |
14 |
14 |
15 consts |
15 consts |
16 ftime,gtime :: nat=>nat |
16 ftime,gtime :: nat=>nat |
17 |
17 |
18 rules |
18 rules |