equal
deleted
inserted
replaced
7 Logic Image: HOL |
7 Logic Image: HOL |
8 |
8 |
9 The temporal level of TLA. |
9 The temporal level of TLA. |
10 *) |
10 *) |
11 |
11 |
12 TLA = Init + WF_Rel + |
12 TLA = Init + |
13 |
13 |
14 consts |
14 consts |
15 (** abstract syntax **) |
15 (** abstract syntax **) |
16 Box :: ('w::world) form => temporal |
16 Box :: ('w::world) form => temporal |
17 Dmd :: ('w::world) form => temporal |
17 Dmd :: ('w::world) form => temporal |
90 eexE "[| sigma |= (EEX x. F x); basevars vs; |
90 eexE "[| sigma |= (EEX x. F x); basevars vs; |
91 (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool) |
91 (!!x. [| basevars (x, vs); sigma |= F x |] ==> (G sigma)::bool) |
92 |] ==> G sigma" |
92 |] ==> G sigma" |
93 history "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)" |
93 history "|- EEX h. Init(h = ha) & [](!x. $h = #x --> h` = hb x)" |
94 end |
94 end |
95 |
|
96 ML |
|