equal
deleted
inserted
replaced
11 types |
11 types |
12 |
12 |
13 'a signature = "('a set * 'a set * 'a set)" |
13 'a signature = "('a set * 'a set * 'a set)" |
14 |
14 |
15 consts |
15 consts |
16 actions,inputs,outputs,internals,externals |
16 actions,inputs,outputs,internals,externals,locals |
17 ::"'action signature => 'action set" |
17 ::"'action signature => 'action set" |
18 is_asig ::"'action signature => bool" |
18 is_asig ::"'action signature => bool" |
19 mk_ext_asig ::"'action signature => 'action signature" |
19 mk_ext_asig ::"'action signature => 'action signature" |
20 |
20 |
21 |
21 |
29 "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))" |
29 "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))" |
30 |
30 |
31 externals_def |
31 externals_def |
32 "externals(asig) == (inputs(asig) Un outputs(asig))" |
32 "externals(asig) == (inputs(asig) Un outputs(asig))" |
33 |
33 |
|
34 locals_def |
|
35 "locals asig == ((internals asig) Un (outputs asig))" |
|
36 |
34 is_asig_def |
37 is_asig_def |
35 "is_asig(triple) == |
38 "is_asig(triple) == |
36 ((inputs(triple) Int outputs(triple) = {}) & |
39 ((inputs(triple) Int outputs(triple) = {}) & |
37 (outputs(triple) Int internals(triple) = {}) & |
40 (outputs(triple) Int internals(triple) = {}) & |
38 (inputs(triple) Int internals(triple) = {}))" |
41 (inputs(triple) Int internals(triple) = {}))" |