equal
deleted
inserted
replaced
8 |
8 |
9 Spec = List + IOA + Action + |
9 Spec = List + IOA + Action + |
10 |
10 |
11 consts |
11 consts |
12 |
12 |
13 spec_sig :: "'m action signature" |
13 spec_sig :: 'm action signature |
14 spec_trans :: "('m action, 'm list)transition set" |
14 spec_trans :: ('m action, 'm list)transition set |
15 spec_ioa :: "('m action, 'm list)ioa" |
15 spec_ioa :: ('m action, 'm list)ioa |
16 |
16 |
17 defs |
17 defs |
18 |
18 |
19 sig_def "spec_sig == (UN m.{S_msg(m)}, |
19 sig_def "spec_sig == (UN m.{S_msg(m)}, |
20 UN m.{R_msg(m)}, |
20 UN m.{R_msg(m)}, |