-
Notifications
You must be signed in to change notification settings - Fork 1
/
solver-loop.maude
74 lines (65 loc) · 2.18 KB
/
solver-loop.maude
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
fmod SOLVER-BANNER is
pr STRING .
op solver-banner : -> String .
eq solver-banner = "L+1 Layers Divide & Conquer Approach to Leads-To and Eventually Model Checking" .
endfm
mod FULL-MAUDE is
pr SOLVER-META-SIGN .
pr SOLVER-DATABASE-HANDLING .
inc LOOP-MODE .
pr FM-BANNER .
pr SOLVER-BANNER .
subsort Object < State .
op o : -> Oid .
op init : -> System .
var Atts : AttributeSet .
var X@DatabaseClass : DatabaseClass .
var O : Oid .
var DB : Database .
var ME : Header .
var QI : Qid .
vars QIL QIL' QIL'' : QidList .
var TL : TermList .
var N : Nat .
vars RP RP' : ResultPair .
rl [init] :
init
=> [nil,
< o : Database |
db : initialDatabase,
input : nilTermList, output : nil,
db-ext : emptyDatabaseExt,
default : 'CONVERSION >,
('\n '\t '\s '\s '\s '\s string2qidList(solver-banner) '\n)] .
rl [in] :
[QI QIL,
< O : X@DatabaseClass |
db : DB, input : nilTermList, output : nil, default : ME, Atts >,
QIL']
=> if metaParse(SOLVER-GRAMMAR, QI QIL, '@Input@) :: ResultPair
then [nil,
< O : X@DatabaseClass | db : DB,
input : getTerm(metaParse(SOLVER-GRAMMAR, QI QIL, '@Input@)),
output : nil, default : ME, Atts >,
QIL']
else [nil,
< O : X@DatabaseClass | db : DB, input : nilTermList,
output : ('\r 'Warning:
printSyntaxError(metaParse(SOLVER-GRAMMAR, QI QIL, '@Input@),
QI QIL)
'\n
'\r 'Error: '\o 'No 'parse 'for 'input. '\n),
default : ME, Atts >,
QIL']
fi .
rl [out] :
[QIL,
< O : X@DatabaseClass |
db : DB, input : TL, output : (QI QIL'), default : ME, Atts >,
QIL'']
=> [QIL,
< O : X@DatabaseClass |
db : DB, input : TL, output : nil, default : ME, Atts >,
(QI QIL' QIL'')] .
endm
loop init .