equal
deleted
inserted
replaced
46 "ask_act == {(s,s'). s'=s | |
46 "ask_act == {(s,s'). s'=s | |
47 (s' = s (|ask := ask s @ [tok s]|) & |
47 (s' = s (|ask := ask s @ [tok s]|) & |
48 size (ask s) = size (rel s))}" |
48 size (ask s) = size (rel s))}" |
49 |
49 |
50 Cli_prg :: state program |
50 Cli_prg :: state program |
51 "Cli_prg == mk_program ({s. tok s : atMost Max & |
51 "Cli_prg == mk_program (UNIV, |
|
52 {s. tok s : atMost Max & |
52 giv s = [] & |
53 giv s = [] & |
53 ask s = [] & |
54 ask s = [] & |
54 rel s = []}, |
55 rel s = []}, |
55 {rel_act, tok_act, ask_act})" |
56 {rel_act, tok_act, ask_act})" |
56 |
57 |