equal
deleted
inserted
replaced
16 minSet :: nat set => nat option |
16 minSet :: nat set => nat option |
17 "minSet A == if A={} then None else Some (LEAST x. x:A)" |
17 "minSet A == if A={} then None else Some (LEAST x. x:A)" |
18 |
18 |
19 rules |
19 rules |
20 |
20 |
21 skip "id: Acts" |
21 skip "id: acts" |
22 |
22 |
23 UC1 "constrains Acts (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))" |
23 UC1 "constrains acts (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))" |
24 |
24 |
25 (* UC1 "constrains Acts {s. minSet s = x} {s. x <= minSet s}" *) |
25 (* UC1 "constrains acts {s. minSet s = x} {s. x <= minSet s}" *) |
26 |
26 |
27 UC2 "leadsTo Acts (minSet -`` {Some x}) {s. x ~: s}" |
27 UC2 "leadsTo acts (minSet -`` {Some x}) {s. x ~: s}" |
28 |
28 |
29 end |
29 end |