Change meta-telingo operator names to long form.

pyproject.toml

@@ -10,12 +10,10 @@ skip_magic_trailing_comma = true
 line-length = 88
 
 [tool.mypy]
-strict = true
 exclude = ["tests/*", "noxfile.py", "init.py"]
 
 [tool.pylsp-mypy]
 enabled = true
 live_mode = true
-strict = true
 exclude = ["tests/*", "noxfile.py", "init.py"]
 

tests/asp/transform/meta-telingo/inputs/input-body.lp

@@ -8,5 +8,5 @@ l :- m.
 e :- prev(prev(b)), until(c,prev(d)).
 a(X) :- until(b(X),next(c(X+Y))) : next(d(Y)); e(X).
 f(X) :- #sum{1:prev(h(Y))} > 3, i(X).
-j(X) :- next(wprev(k(X))).
+j(X) :- next(weak_prev(k(X))).
 

tests/asp/transform/meta-telingo/inputs/input-head.lp

@@ -1,6 +1,6 @@
 #program always.
 a :- initial, b.
 until(c,prev(d)) :- a.
-release(b(X),next(c((X+Y)))): wnext(d(Y)) :- e(X).
+release(b(X),next(c((X+Y)))): weak_next(d(Y)) :- e(X).
 3 < #max { 1: next(j(X)): prev(h(Y)) } :- i(X).
-prev(wprev(k(X))) :- j(X).
+prev(weak_prev(k(X))) :- j(X).

tests/asp/transform/meta-telingo/inputs/input-no-cond.lp

@@ -1,6 +1,6 @@
-until(a(X),b(Y)); not next(c(Y+X)) :- prev(d(X)), eventually(e(Y)).
-f(X) :- wprev(g(X)).
+until(a(X),b(Y)); not next(c(Y+X)) :- prev(d(X)), eventually_after(e(Y)).
+f(X) :- weak_prev(g(X)).
 h(X); i(Y) :- since(j(X),k(Y)).
 h(X); i(Y) :- trigger(j(X),k(Y)).
-prev(l(X)) :- m(X), not n(X), not wprev(o(X)).
+prev(l(X)) :- m(X), not n(X), not weak_prev(o(X)).
 

tests/asp/transform/meta-telingo/inputs/roads.lp

@@ -4,9 +4,9 @@ car(1). car(2).
 road(lisbon,madrid). road(madrid,paris).
 road(boston,ny). road(ny,nj).
 
-wnext(at(X,A)) :- driveto(X,A).
+weak_next(at(X,A)) :- driveto(X,A).
 driveto(X,B); no_driveto(X,B) :- at(X,A), road(A,B).
-wnext(at(X,A)) :- at(X,A), not no_at(X,A).
+weak_next(at(X,A)) :- at(X,A), not no_at(X,A).
 no_at(X,A) :- at(X,B), A!=B, city(A).
 
 :- at(X,A), at(X,B), A!=B.

tests/asp/transform/meta-telingo/meta.lp

@@ -38,10 +38,10 @@ formula(O) :- output(O,_).
 formula(F;G) :- formula(and(F,G);or(F,G);until(F,G);since(F,G)).
 formula(F) :- formula(neg(F);next(F);prev(F)).
 % distinguish operator formulas
-not_atom(X) 
+not_atom(X)
   :- formula(X), 
-		 X=(true;false;initial;final;neg(_);next(_);prev(_);wprev(_);wnext(_);
-				eventually(_);eventually_before(_);always(_);always_before(_);
+		 X=(true;false;initial;final;neg(_);next(_);prev(_);weak_prev(_);weak_next(_);
+				eventually_after(_);eventually_before(_);always_after(_);always_before(_);
 				and(_,_);or(_,_);until(_,_);since(_,_);release(_,_);trigger(_,_)).
 
 #show.
@@ -95,46 +95,46 @@ true(next(F),T) :- true(F,T+1), formula(next(F)), time(T).
 true(F,T-1): time(T-1) :- formula(prev(F)), true(prev(F),T).
 true(prev(F),T) :- true(F,T-1), formula(prev(F)), time(T).
 
-% wprev/1
-define(wprev(F),or(prev(F),initial)) :- formula(wprev(F)).
+% weak_prev/1
+define(weak_prev(F),or(prev(F),initial)) :- formula(weak_prev(F)).
 
-% wnext/1
-define(wnext(F),or(next(F),final)) :- formula(wnext(F)).
+% weak_next/1
+define(weak_next(F),or(next(F),final)) :- formula(weak_next(F)).
 
 % until/2
-true(until(L,R),(T,J)): T<=J, time(J)
+true(until_then(L,R,J),T): T<=J, time(J)
   :- formula(until(L,R)), true(until(L,R),T), time(T).
 true(until(L,R),T)
-  :- formula(until(L,R)), true(until(L,R),(T,_)).
+  :- formula(until(L,R)), true(until_then(L,R,_),T).
 
-true(L,K) :- true(until(L,R),(T,J)), K=T..J-1.
-true(R,J) :- true(until(L,R),(T,J)).
-true(until(L,R),(T,J))
+true(L,K) :- true(until_then(L,R,J),T), K=T..J-1.
+true(R,J) :- true(until_then(L,R,J),T).
+true(until_then(L,R,J),T)
   :- formula(until(L,R)), time(T), time(J), T<=J, true(R,J), 
      true(L,K) : K=T..J-1.
 
 % since/2.
-true(since(L,R),(T,J)): J<=T, time(J)
+true(since_then(L,R,J),T): J<=T, time(J)
   :- formula(since(L,R)), true(since(L,R),T), time(T).
 true(since(L,R),T)
-  :- formula(since(L,R)), true(since(L,R),(T,_)).
+  :- formula(since(L,R)), true(since_then(L,R,_),T).
 
-true(L,K) :- true(since(L,R),(T,J)), K=J+1..T.
-true(R,J) :- true(since(L,R),(T,J)).
-true(since(L,R),(T,J))
+true(L,K) :- true(since(L,R,J),T), K=J+1..T.
+true(R,J) :- true(since(L,R,J),T).
+true(since(L,R,J),T)
   :- formula(since(L,R)), time(T), time(J), J<=T, true(R,J), 
      true(L,K) : K=J+1..T.
 
-% eventually/1
-define(eventually(F),until(true,F)) :- formula(eventually(F)).
+% eventually_after/1
+define(eventually_after(F),until(true,F)) :- formula(eventually_after(F)).
 % eventually_before/1
 define(eventually_before(F),since(true,F)) :- formula(eventually_before(F)).
 
 % define derived operators
 % release/2
 define(release(L,R),until(R,and(R,or(L,final)))) :- formula(release(L,R)).
-% always/1
-define(always(F),release(false,F)) :- formula(always(F)).
+% always_after/1
+define(always_after(F),release(false,F)) :- formula(always_after(F)).
 % trigger/2
 define(trigger(L,R),since(R,and(R,or(L,initial)))) :- formula(trigger(L,R)).
 % always_before/1

tests/asp/transform/meta-telingo/outputs/output-body.lp

@@ -8,7 +8,7 @@ l :- not initial; m.
 e :- prev(prev(b)); until(c,prev(d)).
 a(X) :- until(b(X),next(c((X+Y)))): next(d(Y)); e(X).
 f(X) :- 3 < #sum { 1: prev(h(Y)) }; i(X).
-j(X) :- next(wprev(k(X))).
+j(X) :- next(weak_prev(k(X))).
 #program base.
 #external initial. [false]
 #external initial. [false]
@@ -18,4 +18,4 @@ j(X) :- next(wprev(k(X))).
 #external until(b(X),next(c((X+Y)))) : d(Y); e(X). [false]
 #external next(d(Y)) : d(Y); e(X). [false]
 #external prev(h(Y)) : h(Y); i(X). [false]
-#external next(wprev(k(X))). [false]
+#external next(weak_prev(k(X))). [false]

tests/asp/transform/meta-telingo/outputs/output-head.lp

@@ -1,12 +1,12 @@
 #program base.
 a :- initial; b.
 until(c,prev(d)) :- a.
-release(b(X),next(c((X+Y)))): wnext(d(Y)) :- e(X).
+release(b(X),next(c((X+Y)))): weak_next(d(Y)) :- e(X).
 3 < #max { 1: next(j(X)): prev(h(Y)) } :- i(X).
-prev(wprev(k(X))) :- j(X).
+prev(weak_prev(k(X))) :- j(X).
 #program base.
 #external initial. [false]
-#external wnext(d(Y)) : e(X). [false]
+#external weak_next(d(Y)) : e(X). [false]
 #external prev(h(Y)) : h(Y); i(X). [false]
 #external c : a. [false]
 #external d : a. [false]

tests/asp/transform/meta-telingo/outputs/output-no-cond.lp

@@ -1,15 +1,15 @@
-until(a(X),b(Y)); not next(c((Y+X))) :- prev(d(X)); eventually(e(Y)).
-f(X) :- wprev(g(X)).
+until(a(X),b(Y)); not next(c((Y+X))) :- prev(d(X)); eventually_after(e(Y)).
+f(X) :- weak_prev(g(X)).
 h(X); i(Y) :- since(j(X),k(Y)).
 h(X); i(Y) :- trigger(j(X),k(Y)).
-prev(l(X)) :- m(X); not n(X); not wprev(o(X)).
+prev(l(X)) :- m(X); not n(X); not weak_prev(o(X)).
 #program base.
 #external prev(d(X)) : d(X); e(Y). [false]
-#external eventually(e(Y)) : d(X); e(Y). [false]
-#external wprev(g(X)). [false]
+#external eventually_after(e(Y)) : d(X); e(Y). [false]
+#external weak_prev(g(X)). [false]
 #external since(j(X),k(Y)) : k(Y). [false]
 #external trigger(j(X),k(Y)) : k(Y). [false]
-#external wprev(o(X)) : m(X). [false]
+#external weak_prev(o(X)) : m(X). [false]
 #external a(X) : d(X); e(Y). [false]
 #external b(Y) : d(X); e(Y). [false]
 #external c((Y+X)) : d(X); e(Y). [false]

tests/asp/transform/meta-telingo/outputs/telingo-output.lp

@@ -34,7 +34,7 @@
   &tel/0: formula, any
 }.
 #program base.
-eventually(fail(X)) :- and(and(shoot(X),prev(eventually_before(shoot(X)))),always_before(unloaded(X))).
+eventually_after(fail(X)) :- and(and(shoot(X),prev(eventually_before(shoot(X)))),always_before(unloaded(X))).
 and(and(and(shoot(X),unloaded(X)),next(unloaded(X))),next(next(until(unloaded(X),prev(shoot(X)))))) :- and(initial,firearm(X)).
 firearm(gun).
 #show show(shoot(X)) : shoot(X).

tests/asp/transform/meta-telingo/transform-add-externals-no-condition.lp

@@ -1,11 +1,11 @@
 operator_arity((initial;final),0).
-operator_arity((prev;wprev;next;wnext;neg;
-							 always;always_before;eventually;eventually_before),1).
+operator_arity((prev;weak_prev;next;weak_next;neg;
+							 always_after;always_before;eventually_after;eventually_before),1).
 operator_arity((until;since;release;trigger;and;or),2).
 % Naturally, default negation is unsafe.
-% wnext/wprev are unsafe, as they are satisfied in the final/initial time step
+% weak_next/weak_prev are unsafe, as they are satisfied in the final/initial time step
 % even if their operand is not.
-arg((wprev;wnext),0,unsafe).
+arg((weak_prev;weak_next),0,unsafe).
 % the left operand of binary temporal operators are considered unsafe,
 % as they can be satisfied even if their left operand is not.
 arg((until;since;release;trigger),0,unsafe).

tests/asp/transform/meta-telingo/transform-add-externals.lp

@@ -1,11 +1,11 @@
 operator_arity((initial;final),0).
-operator_arity((prev;wprev;next;wnext;neg;
-							 always;always_before;eventually;eventually_before),1).
+operator_arity((prev;weak_prev;next;weak_next;neg;
+							 always_after;always_before;eventually_after;eventually_before),1).
 operator_arity((until;since;release;trigger;and;or),2).
 % Naturally, default negation is unsafe.
-% wnext/wprev are unsafe, as they are satisfied in the final/initial time step
+% weak_next/weak_prev are unsafe, as they are satisfied in the final/initial time step
 % even if their operand is not.
-arg((wprev;wnext),0,unsafe).
+arg((weak_prev;weak_next),0,unsafe).
 % the left operand of binary temporal operators are considered unsafe,
 % as they can be satisfied even if their left operand is not.
 arg((until;since;release;trigger),0,unsafe).

tests/asp/transform/meta-telingo/transform-theory-to-symbolic.lp

@@ -1,6 +1,6 @@
 theory_opertor2symbol(
-  "<",1,prev ; "<:",1,wprev ; "<?",1,eventually_before; "<*",1,always_before ;
-	 ">",1,next ; ">:",1,wnext ; ">?",1,eventually ; ">*",1,always ;
+  "<",1,prev ; "<:",1,weak_prev ; "<?",1,eventually_before; "<*",1,always_before ;
+	 ">",1,next ; ">:",1,weak_next ; ">?",1,eventually_after ; ">*",1,always_after ;
 	 ">*",2,release ; ">?",2,until ; "<*",2,trigger ; "<?",2,since ;
 	 "&",1,keyword_prefix ; "~",1,neg ; "&",2,and ; "|",2,or 
 ).