| changeset 7537 | 875754b599df |
| parent 5648 | fe887910e32e |
| child 10064 | 1a77667b21ef |
| 7536:5c094aec523d | 7537:875754b599df |
|---|---|
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 = SubstAx + Union + |
13 Common = Union + |
14 |
14 |
15 consts |
15 consts |
16 ftime,gtime :: nat=>nat |
16 ftime,gtime :: nat=>nat |
17 |
17 |
18 rules |
18 rules |