|
7
|
1 package lite;
|
|
|
2
|
|
32
|
3 import java.util.LinkedList;
|
|
|
4
|
|
74
|
5 import parser.Command;
|
|
|
6 import parser.Dictionary;
|
|
|
7 import parser.LogicNodeScope;
|
|
|
8 import parser.MacroNodeParser;
|
|
|
9 import parser.Token;
|
|
|
10 import parser.TokenID;
|
|
|
11
|
|
67
|
12 import sbdd.SBDDFactory;
|
|
|
13
|
|
7
|
14
|
|
31
|
15 public class ITLNodeParser<Node extends ITLSolver> extends MacroNodeParser<Node> {
|
|
7
|
16
|
|
|
17 public ITLNodeFactoryInterface<Node> logicNodeFactory;
|
|
|
18 public ITLNodeScanner<Node> scanner;
|
|
59
|
19 public ITLCommander<Node> parseCommand;
|
|
55
|
20 public Node emptyNode;
|
|
67
|
21 private Node periodNode;
|
|
73
|
22 public String help = "";
|
|
7
|
23
|
|
|
24 public ITLNodeParser(ITLNodeFactoryInterface<Node> lf) {
|
|
33
|
25
|
|
30
|
26 super(lf);
|
|
7
|
27 logicNodeFactory = lf;
|
|
|
28 initialize();
|
|
33
|
29
|
|
|
30 Token<Node> emptyToken = dict.reserve("empty",TokenID.Empty);
|
|
55
|
31 emptyNode = emptyToken.value = logicNodeFactory.emptyNode();
|
|
23
|
32
|
|
57
|
33 parseCommand = new ITLCommander<Node>(lf,this);
|
|
23
|
34
|
|
31
|
35 define("not(P)","~P"); // not
|
|
84
|
36 define("P->Q","(not(P);Q))",101); // imply
|
|
31
|
37 define("P<->Q","((not(P);Q),(P; not(Q)))"); // equiv
|
|
|
38 define("P=Q","((not(P);Q),(P; not(Q)))"); // equiv
|
|
84
|
39 // P&&Q have to be left associative ( xfy i.e. a&&b&&c = a&&(b&&c)
|
|
|
40 // odd order means xfy associativity. & is right associative (yfx) in this
|
|
|
41 // parser, but & has associative, so it is alright. (&& is not assosicative)
|
|
|
42 define("P && Q","((not(empty),P) & Q))",901); // strong chop
|
|
19
|
43 define("'<>'(Q)","(true & Q))"); // sometime
|
|
|
44 define("'#'(Q)"," not(true & not(Q)))"); // always
|
|
|
45 define("'[]'(Q)"," not(true & not(Q)))"); // always
|
|
|
46 define("'[a]'(Q)"," not(true & not(Q) & true))"); // always with arbitary fin
|
|
|
47 define("'<a>'(Q)"," (true & Q & true))"); // sometime with arbitary fin
|
|
|
48 define("fin(Q)","(true & (empty,Q)))"); // final state in the interval
|
|
|
49 define("keep(Q)"," not(true & not((empty ; Q))))"); // except final state
|
|
|
50 define("halt(Q)"," '[]'(empty=Q))");
|
|
|
51 define("more"," not(empty))"); // non empty interval
|
|
|
52 // discrete stuff
|
|
|
53 define("skip"," @(empty))"); // 1 length interval
|
|
|
54 define("infinite"," (true & false))"); //
|
|
|
55 define("finite"," ~((true & false)))"); //
|
|
59
|
56 // define("length(I)", "true",50,command); // length operator
|
|
|
57 define("length(I)", "empty",50, // length operator
|
|
58
|
58 new Command<Node>() {
|
|
|
59 public Node exec(Node predicate, Node value, LinkedList<Node> args) {
|
|
|
60 Node n = value;
|
|
|
61 int length = Integer.parseInt(args.get(0).toString());
|
|
|
62 for(int i =0;i<length;i++) {
|
|
73
|
63 n = logicNodeFactory.nextNode(n);
|
|
|
64 n=logicNodeFactory.andNode(
|
|
|
65 logicNodeFactory.notNode(
|
|
|
66 logicNodeFactory.emptyNode())
|
|
|
67 ,n);
|
|
58
|
68 }
|
|
65
|
69 return n;
|
|
58
|
70 }
|
|
|
71 });
|
|
59
|
72 define("less(I)","false",50,parseCommand); // less than N length
|
|
73
|
73 define("@(P)","(~empty, next(P)))");
|
|
19
|
74 // temporal assignments
|
|
|
75 define("gets(A,B)","keep(@A<->B))");
|
|
|
76 define("stable(A)","keep(@A<->A))");
|
|
|
77 // define("state(A)","(share(A),'[]'(L))):- def_state(A,L)");
|
|
|
78 // def(Q=>P,exists(R,(Q = R,stable(R),fin(P = R))))");
|
|
|
79 // easier one
|
|
|
80 define("Q=>P","(Q & (empty,P); ~Q & (empty, ~P)))");
|
|
|
81 // def(P<=Q,Q=>P)");
|
|
|
82 // loop stuff and quantifiers
|
|
65
|
83 define("*(A) ","proj(A,true),fin(A)"); // weak closure
|
|
69
|
84 // define("+(A) ","A& *(empty;A)"); // strong closure (difficult one)
|
|
|
85 define("+(A) ","A & proj(A,true)"); // strong closure
|
|
19
|
86 define("while(Cond,Do)"," *(((Cond->Do) , (~Cond->empty))))");
|
|
|
87 define("repeat(Do,until,Cond)"," (*((Do;empty)) ,@ halt(Cond)))");
|
|
|
88 define("all(P,Q)","not(exists(P,not(Q)))");
|
|
31
|
89 define("local(P)"," (P = (P&true))");
|
|
19
|
90 // test predicates
|
|
|
91 // define("trace(X,List),L) :- !,make_trace(List,X,L)");
|
|
|
92 define("even(P)","exists(Q,(Q, keep( @Q = ~Q),'[]'((Q->P)))))");
|
|
|
93 define("evenp(P)","(*(((P,skip) & skip;empty,P)) & (empty;skip)))");
|
|
|
94 define("phil(L,R)","+('[]'((~L, ~R)) & @ (L, ~R,@ (L,R, @ (R,'[]'( ~L)))) ))");
|
|
65
|
95
|
|
27
|
96 define("ex(N,Exp)","true",50,parseCommand);
|
|
70
|
97 define("do(N)","true",50,parseCommand);
|
|
73
|
98 define("diag(N)","true",50,parseCommand);
|
|
|
99 define("exe(N)","true",50,parseCommand);
|
|
71
|
100 define("def(Head,Body)","true",50,parseCommand);
|
|
57
|
101 define("include(path)","true",50,parseCommand);
|
|
59
|
102
|
|
65
|
103 define("ex0(N,Exp)","skipped");
|
|
|
104 define("verbose(I)", "true",50,parseCommand);
|
|
|
105
|
|
59
|
106 define("^(r)","r"); // interval variable (we cannot handle now)
|
|
67
|
107
|
|
|
108 periodNode = logicNodeFactory.variableNode(".", true);
|
|
73
|
109 define("help","true",50,parseCommand);
|
|
88
|
110 define("show","true",50,parseCommand);
|
|
|
111 define("states","true",50,parseCommand);
|
|
|
112 define("ls","true",50,parseCommand);
|
|
|
113 define("clear","true",50,parseCommand);
|
|
67
|
114 // only one of the is true (should allow all false case?)
|
|
|
115 define("share(L)","[](share0(L))");
|
|
|
116 define("share0(L)","true",50, new Command<Node>() {
|
|
74
|
117 @SuppressWarnings("unchecked")
|
|
67
|
118 public Node exec(Node predicate, Node value, LinkedList<Node> args) {
|
|
|
119 Node allFalse = (Node)SBDDFactory.trueSolver;
|
|
|
120 value= (Node)SBDDFactory.falseSolver;
|
|
|
121 LinkedList<ITLSolver> list = args.get(0).arguments();
|
|
69
|
122 if (list==null) {
|
|
|
123 error("sahre: missing [] argument");
|
|
|
124 return value;
|
|
|
125 }
|
|
67
|
126 if (list.isEmpty()) return value;
|
|
|
127 for(ITLSolver n: list) {
|
|
|
128 Node n1 = (Node)n;
|
|
|
129 value = logicNodeFactory.bddNode(n1, allFalse, value);
|
|
|
130 allFalse = logicNodeFactory.bddNode(n1,
|
|
|
131 (Node)SBDDFactory.falseSolver,allFalse);
|
|
|
132 }
|
|
|
133 return value;
|
|
|
134 }
|
|
|
135 });
|
|
19
|
136
|
|
7
|
137 }
|
|
|
138
|
|
|
139 public ITLNodeParser() {
|
|
|
140 super();
|
|
|
141 }
|
|
11
|
142
|
|
|
143
|
|
|
144 @Override
|
|
|
145 public void initialize() {
|
|
|
146 dict = new Dictionary<Node>();
|
|
28
|
147 scope = new LogicNodeScope<Node>(null,dict);
|
|
11
|
148 initReservedWord();
|
|
|
149 scanner = new ITLNodeScanner<Node>(dict);
|
|
30
|
150 super.scanner = scanner;
|
|
29
|
151
|
|
|
152 dict.reserve("&",TokenID.Chop);
|
|
73
|
153 dict.reserve("next",TokenID.Next);
|
|
57
|
154 dict.reserve("proj",TokenID.Projection);
|
|
31
|
155
|
|
88
|
156 // parseCommand requires compile tme reserved word for string comparison
|
|
67
|
157 dict.reserve("less");
|
|
|
158 dict.reserve("ex");
|
|
70
|
159 dict.reserve("do");
|
|
67
|
160 dict.reserve("include");
|
|
|
161 dict.reserve("def");
|
|
|
162 dict.reserve("verbose");
|
|
73
|
163 dict.reserve("help");
|
|
|
164 dict.reserve("diag");
|
|
|
165 dict.reserve("exe");
|
|
88
|
166 dict.reserve("show");
|
|
|
167 dict.reserve("ls");
|
|
|
168 dict.reserve("states");
|
|
|
169 dict.reserve("clear");
|
|
11
|
170 }
|
|
20
|
171
|
|
30
|
172 @Override
|
|
|
173 public Node expr2() {
|
|
|
174 Node n = exprI2();
|
|
32
|
175 while(nextToken.type==TokenID.And) {
|
|
30
|
176 nextToken();
|
|
32
|
177 n = logicNodeFactory.andNode(n, exprI2()) ;
|
|
30
|
178 }
|
|
|
179 return n;
|
|
|
180 }
|
|
31
|
181
|
|
60
|
182 @Override
|
|
67
|
183 public Node expr3() {
|
|
71
|
184 if (nextToken.type == TokenID.Next) {
|
|
|
185 nextToken();
|
|
|
186 return logicNodeFactory.nextNode(expr3());
|
|
|
187 }
|
|
67
|
188 Node n = super.expr3();
|
|
|
189 while(nextToken.type==TokenID.Question) {
|
|
|
190 nextToken();
|
|
|
191 Node cond = n;
|
|
|
192 Node high = expr3();
|
|
|
193 if (nextToken.type!=TokenID.Colon) {
|
|
|
194 error(": expected");
|
|
|
195 return logicNodeFactory.trueNode();
|
|
|
196 }
|
|
|
197 nextToken();
|
|
|
198 Node low = expr3();
|
|
|
199 n = logicNodeFactory.orNode(
|
|
|
200 logicNodeFactory.andNode(cond, high),
|
|
|
201 logicNodeFactory.andNode(logicNodeFactory.notNode(cond), low));
|
|
|
202 }
|
|
|
203 return n;
|
|
|
204 }
|
|
|
205
|
|
30
|
206
|
|
67
|
207 @Override
|
|
|
208 public Node term() {
|
|
|
209 if (nextToken.type==TokenID.BParen) {
|
|
|
210 Node predicate = periodNode;
|
|
|
211 nextToken();
|
|
|
212 LinkedList<Node> arg = arguments();
|
|
|
213 return logicNodeFactory.predicateNode(predicate, arg);
|
|
|
214 }
|
|
|
215 return super.term();
|
|
|
216 }
|
|
|
217
|
|
34
|
218 public Node exprI2() {
|
|
60
|
219 Node n = exprM1();
|
|
32
|
220 while(nextToken.type == TokenID.Chop) {
|
|
30
|
221 nextToken();
|
|
60
|
222 n = logicNodeFactory.chopNode(n, exprM1());
|
|
30
|
223 }
|
|
|
224 return n;
|
|
|
225 }
|
|
31
|
226
|
|
32
|
227
|
|
|
228 @Override
|
|
|
229 protected LinkedList<Node> arguments() {
|
|
|
230 Node n;
|
|
|
231 LinkedList<Node> arg = new LinkedList<Node>();
|
|
67
|
232 while(nextToken.type!=TokenID.CloseParen&&nextToken.type!=TokenID.CloseBParen) {
|
|
64
|
233 if (nextToken.type==TokenID.NULL) break;
|
|
32
|
234 n = exprI2();
|
|
|
235 arg.add(n);
|
|
|
236 if (nextToken.type == TokenID.And)
|
|
|
237 nextToken();
|
|
|
238 }
|
|
67
|
239 if (nextToken.type==TokenID.CloseParen||
|
|
|
240 nextToken.type==TokenID.CloseBParen) nextToken();
|
|
32
|
241 else {
|
|
|
242 scanner.error(") expected");
|
|
|
243 }
|
|
|
244 return arg;
|
|
|
245 }
|
|
71
|
246
|
|
33
|
247 public ITLSolver emptyNode() {
|
|
|
248 return emptyNode;
|
|
|
249 }
|
|
57
|
250
|
|
73
|
251 public void addHelp(String string) {
|
|
|
252 help += string;
|
|
|
253 }
|
|
|
254
|
|
|
255 public void help() {
|
|
|
256 System.out.println(help);
|
|
|
257 }
|
|
|
258
|
|
70
|
259
|
|
88
|
260
|
|
7
|
261 }
|
