From 813c3799c0f9cca81e70251fa10f8da2b792f911 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Sat, 20 Jun 2015 14:48:07 +0200 Subject: [PATCH] ltl: remove is_eltl_formula() * doc/tl/tl.tex, src/ltlast/atomic_prop.cc, src/ltlast/binop.cc, src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/formula.cc, src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/unop.cc: Remove is_eltl_formula(). * src/tests/kind.test: Adjust. --- doc/tl/tl.tex | 2 -- src/ltlast/atomic_prop.cc | 1 - src/ltlast/binop.cc | 6 ------ src/ltlast/bunop.cc | 1 - src/ltlast/constant.cc | 2 -- src/ltlast/formula.cc | 1 - src/ltlast/formula.hh | 7 ------- src/ltlast/multop.cc | 2 -- src/ltlast/unop.cc | 5 ----- src/tests/kind.test | 12 ++++++------ 10 files changed, 6 insertions(+), 33 deletions(-) diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index a1b546bdf..3de918c20 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -1048,8 +1048,6 @@ instance using the following methods: Whether the formula avoids the $\X$ operator. \\\texttt{is\_ltl\_formula()}& Whether the formula uses only LTL operators. (Boolean operators are also allowed.) -\\\texttt{is\_eltl\_formula()}& Whether the formula uses only ELTL - operators. (Boolean and LTL operators are also allowed.) \\\texttt{is\_psl\_formula()}& Whether the formula uses only PSL operators. (Boolean and LTL operators are also allowed.) \\\texttt{is\_sere\_formula()}& Whether the formula uses only diff --git a/src/ltlast/atomic_prop.cc b/src/ltlast/atomic_prop.cc index 139be1f6e..7e0bfdf83 100644 --- a/src/ltlast/atomic_prop.cc +++ b/src/ltlast/atomic_prop.cc @@ -45,7 +45,6 @@ namespace spot // matters.) is.sugar_free_ltl = true; is.ltl_formula = true; - is.eltl_formula = true; is.psl_formula = true; is.sere_formula = true; is.finite = true; diff --git a/src/ltlast/binop.cc b/src/ltlast/binop.cc index 30edb26c8..60776a094 100644 --- a/src/ltlast/binop.cc +++ b/src/ltlast/binop.cc @@ -111,7 +111,6 @@ namespace spot is.not_marked = (op != EConcatMarked); is.ltl_formula = false; is.boolean = false; - is.eltl_formula = false; is.sere_formula = false; is.accepting_eword = false; is.psl_formula = true; @@ -139,7 +138,6 @@ namespace spot is.not_marked = true; is.ltl_formula = false; is.boolean = false; - is.eltl_formula = false; is.sere_formula = false; is.accepting_eword = false; is.psl_formula = true; @@ -169,7 +167,6 @@ namespace spot is.eventual = second->is_eventual(); is.eventual |= (first == constant::true_instance()); is.boolean = false; - is.eltl_formula = false; is.sere_formula = false; is.finite = false; is.accepting_eword = false; @@ -189,7 +186,6 @@ namespace spot // f W g is universal if f and g are, or if g == 0. is.universal |= (second == constant::false_instance()); is.boolean = false; - is.eltl_formula = false; is.sere_formula = false; is.finite = false; is.accepting_eword = false; @@ -210,7 +206,6 @@ namespace spot is.universal = second->is_universal(); is.universal |= (first == constant::false_instance()); is.boolean = false; - is.eltl_formula = false; is.sere_formula = false; is.finite = false; is.accepting_eword = false; @@ -230,7 +225,6 @@ namespace spot // g M f is eventual if both g and f are eventual, or if f == 1. is.eventual |= (second == constant::true_instance()); is.boolean = false; - is.eltl_formula = false; is.sere_formula = false; is.finite = false; is.accepting_eword = false; diff --git a/src/ltlast/bunop.cc b/src/ltlast/bunop.cc index fb6b724d4..2801dddbb 100644 --- a/src/ltlast/bunop.cc +++ b/src/ltlast/bunop.cc @@ -43,7 +43,6 @@ namespace spot assert(is.sere_formula); is.boolean = false; is.ltl_formula = false; - is.eltl_formula = false; is.psl_formula = false; is.eventual = false; is.universal = false; diff --git a/src/ltlast/constant.cc b/src/ltlast/constant.cc index 409c47f40..a19722877 100644 --- a/src/ltlast/constant.cc +++ b/src/ltlast/constant.cc @@ -46,7 +46,6 @@ namespace spot is.syntactic_si = true; // for LTL (not PSL) is.sugar_free_ltl = true; is.ltl_formula = true; - is.eltl_formula = true; is.psl_formula = true; is.sere_formula = true; is.finite = true; @@ -69,7 +68,6 @@ namespace spot is.syntactic_si = true; is.sugar_free_ltl = true; is.ltl_formula = false; - is.eltl_formula = false; is.psl_formula = false; is.sere_formula = true; is.finite = true; diff --git a/src/ltlast/formula.cc b/src/ltlast/formula.cc index c2b92f52b..07ad14995 100644 --- a/src/ltlast/formula.cc +++ b/src/ltlast/formula.cc @@ -43,7 +43,6 @@ namespace spot "syntactic stutter invariant"); \ proprint(is_sugar_free_ltl, "f", "without LTL sugar"); \ proprint(is_ltl_formula, "L", "LTL formula"); \ - proprint(is_eltl_formula, "E", "ELTL formula"); \ proprint(is_psl_formula, "P", "PSL formula"); \ proprint(is_sere_formula, "S", "SERE formula"); \ proprint(is_finite, "F", "finite"); \ diff --git a/src/ltlast/formula.hh b/src/ltlast/formula.hh index c42c513bd..e1f8f702b 100644 --- a/src/ltlast/formula.hh +++ b/src/ltlast/formula.hh @@ -170,12 +170,6 @@ namespace spot return is.ltl_formula; } - /// Whether the formula uses only ELTL operators. - bool is_eltl_formula() const - { - return is.eltl_formula; - } - /// Whether the formula uses only PSL operators. bool is_psl_formula() const { @@ -344,7 +338,6 @@ namespace spot bool syntactic_si:1; // LTL-X or siPSL bool sugar_free_ltl:1; // No F and G operators. bool ltl_formula:1; // Only LTL operators. - bool eltl_formula:1; // Only ELTL operators. bool psl_formula:1; // Only PSL operators. bool sere_formula:1; // Only SERE operators. bool finite:1; // Finite SERE formulae, or Bool+X forms. diff --git a/src/ltlast/multop.cc b/src/ltlast/multop.cc index 4c3f80b4b..b632b7d3a 100644 --- a/src/ltlast/multop.cc +++ b/src/ltlast/multop.cc @@ -60,7 +60,6 @@ namespace spot // NOT Boolean. is.boolean = false; is.ltl_formula = false; - is.eltl_formula = false; is.psl_formula = false; is.eventual = false; is.universal = false; @@ -88,7 +87,6 @@ namespace spot // and the result is therefore NOT Boolean. is.boolean = false; is.ltl_formula = false; - is.eltl_formula = false; is.psl_formula = false; is.eventual = false; is.universal = false; diff --git a/src/ltlast/unop.cc b/src/ltlast/unop.cc index 208916b0b..9473345c1 100644 --- a/src/ltlast/unop.cc +++ b/src/ltlast/unop.cc @@ -59,7 +59,6 @@ namespace spot is.not_marked = true; is.boolean = false; is.syntactic_si = false; - is.eltl_formula = false; is.sere_formula = false; // is.syntactic_safety inherited // is.syntactic_guarantee inherited @@ -71,7 +70,6 @@ namespace spot case F: is.not_marked = true; is.boolean = false; - is.eltl_formula = false; is.sere_formula = false; is.finite = false; is.sugar_free_ltl = false; @@ -86,7 +84,6 @@ namespace spot case G: is.not_marked = true; is.boolean = false; - is.eltl_formula = false; is.sere_formula = false; is.finite = false; is.sugar_free_ltl = false; @@ -103,7 +100,6 @@ namespace spot is.not_marked = (op == NegClosure); is.boolean = false; is.ltl_formula = false; - is.eltl_formula = false; is.psl_formula = true; is.sere_formula = false; is.syntactic_safety = is.finite; @@ -119,7 +115,6 @@ namespace spot is.not_marked = true; is.boolean = false; is.ltl_formula = false; - is.eltl_formula = false; is.psl_formula = true; is.sere_formula = false; is.syntactic_safety = true; diff --git a/src/tests/kind.test b/src/tests/kind.test index 603c58a9c..09a4824cf 100755 --- a/src/tests/kind.test +++ b/src/tests/kind.test @@ -26,10 +26,10 @@ set -e cat >input<b,BxfLEPSFsgopra -!a,B&!xfLEPSFsgopra -!(a|b),B&xfLEPSFsgopra +a,B&!xfLPSFsgopra +a<->b,BxfLPSFsgopra +!a,B&!xfLPSFsgopra +!(a|b),B&xfLPSFsgopra F(a),&!xLPegopra G(a),&!xLPusopra a U b,&!xfLPgopra @@ -95,8 +95,8 @@ Fa -> Gb,xLPsopra {a;c|d;b}<>->GFb,&!Pra {a;c|d;_b}<>->!FGb,&Pr # Equivalent to a&b&c&d -{a:b:c:d}!,B&!xfLEPSFsgopra -a&b&c&d,B&!xfLEPSFsgopra +{a:b:c:d}!,B&!xfLPSFsgopra +a&b&c&d,B&!xfLPSFsgopra (Xa <-> XXXc) U (b & Fe),LPgopra (!X(a|X(!b))&(FX(g xor h)))U(!G(a|b)),LPegopra (!X(a|X(!b))&(GX(g xor h)))R(!F(a|b)),LPusopra