alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

ltl: remove is_eltl_formula()

Browse source 
* 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.
This commit is contained in:
Alexandre Duret-Lutz 2015-06-20 14:48:07 +02:00
parent ce3ad1e3ff
commit 813c3799c0
10 changed files with 6 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

2
doc/tl/tl.tex
View file

@ -1048,8 +1048,6 @@ instance using the following methods:
Whether the formula avoids the $\X$ operator. Whether the formula avoids the $\X$ operator.
\\\texttt{is\_ltl\_formula()}& Whether the formula uses only LTL \\\texttt{is\_ltl\_formula()}& Whether the formula uses only LTL
operators. (Boolean operators are also allowed.) 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 \\\texttt{is\_psl\_formula()}& Whether the formula uses only PSL
operators. (Boolean and LTL operators are also allowed.) operators. (Boolean and LTL operators are also allowed.)
\\\texttt{is\_sere\_formula()}& Whether the formula uses only \\\texttt{is\_sere\_formula()}& Whether the formula uses only

1
src/ltlast/atomic_prop.cc
View file

@ -45,7 +45,6 @@ namespace spot
// matters.) // matters.)
is.sugar_free_ltl = true; is.sugar_free_ltl = true;
is.ltl_formula = true; is.ltl_formula = true;
is.eltl_formula = true;
is.psl_formula = true; is.psl_formula = true;
is.sere_formula = true; is.sere_formula = true;
is.finite = true; is.finite = true;

6
src/ltlast/binop.cc
View file

@ -111,7 +111,6 @@ namespace spot
is.not_marked = (op != EConcatMarked); is.not_marked = (op != EConcatMarked);
is.ltl_formula = false; is.ltl_formula = false;
is.boolean = false; is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false; is.sere_formula = false;
is.accepting_eword = false; is.accepting_eword = false;
is.psl_formula = true; is.psl_formula = true;
@ -139,7 +138,6 @@ namespace spot
is.not_marked = true; is.not_marked = true;
is.ltl_formula = false; is.ltl_formula = false;
is.boolean = false; is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false; is.sere_formula = false;
is.accepting_eword = false; is.accepting_eword = false;
is.psl_formula = true; is.psl_formula = true;
@ -169,7 +167,6 @@ namespace spot
is.eventual = second->is_eventual(); is.eventual = second->is_eventual();
is.eventual |= (first == constant::true_instance()); is.eventual |= (first == constant::true_instance());
is.boolean = false; is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false; is.sere_formula = false;
is.finite = false; is.finite = false;
is.accepting_eword = 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. // f W g is universal if f and g are, or if g == 0.
is.universal |= (second == constant::false_instance()); is.universal |= (second == constant::false_instance());
is.boolean = false; is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false; is.sere_formula = false;
is.finite = false; is.finite = false;
is.accepting_eword = false; is.accepting_eword = false;
@ -210,7 +206,6 @@ namespace spot
is.universal = second->is_universal(); is.universal = second->is_universal();
is.universal |= (first == constant::false_instance()); is.universal |= (first == constant::false_instance());
is.boolean = false; is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false; is.sere_formula = false;
is.finite = false; is.finite = false;
is.accepting_eword = 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. // g M f is eventual if both g and f are eventual, or if f == 1.
is.eventual |= (second == constant::true_instance()); is.eventual |= (second == constant::true_instance());
is.boolean = false; is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false; is.sere_formula = false;
is.finite = false; is.finite = false;
is.accepting_eword = false; is.accepting_eword = false;

1
src/ltlast/bunop.cc
View file

@ -43,7 +43,6 @@ namespace spot
assert(is.sere_formula); assert(is.sere_formula);
is.boolean = false; is.boolean = false;
is.ltl_formula = false; is.ltl_formula = false;
is.eltl_formula = false;
is.psl_formula = false; is.psl_formula = false;
is.eventual = false; is.eventual = false;
is.universal = false; is.universal = false;

2
src/ltlast/constant.cc
View file

@ -46,7 +46,6 @@ namespace spot
is.syntactic_si = true; // for LTL (not PSL) is.syntactic_si = true; // for LTL (not PSL)
is.sugar_free_ltl = true; is.sugar_free_ltl = true;
is.ltl_formula = true; is.ltl_formula = true;
is.eltl_formula = true;
is.psl_formula = true; is.psl_formula = true;
is.sere_formula = true; is.sere_formula = true;
is.finite = true; is.finite = true;
@ -69,7 +68,6 @@ namespace spot
is.syntactic_si = true; is.syntactic_si = true;
is.sugar_free_ltl = true; is.sugar_free_ltl = true;
is.ltl_formula = false; is.ltl_formula = false;
is.eltl_formula = false;
is.psl_formula = false; is.psl_formula = false;
is.sere_formula = true; is.sere_formula = true;
is.finite = true; is.finite = true;

1
src/ltlast/formula.cc
View file

@ -43,7 +43,6 @@ namespace spot
"syntactic stutter invariant"); \ "syntactic stutter invariant"); \
proprint(is_sugar_free_ltl, "f", "without LTL sugar"); \ proprint(is_sugar_free_ltl, "f", "without LTL sugar"); \
proprint(is_ltl_formula, "L", "LTL formula"); \ proprint(is_ltl_formula, "L", "LTL formula"); \
proprint(is_eltl_formula, "E", "ELTL formula"); \
proprint(is_psl_formula, "P", "PSL formula"); \ proprint(is_psl_formula, "P", "PSL formula"); \
proprint(is_sere_formula, "S", "SERE formula"); \ proprint(is_sere_formula, "S", "SERE formula"); \
proprint(is_finite, "F", "finite"); \ proprint(is_finite, "F", "finite"); \

7
src/ltlast/formula.hh
View file

@ -170,12 +170,6 @@ namespace spot
return is.ltl_formula; 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. /// Whether the formula uses only PSL operators.
bool is_psl_formula() const bool is_psl_formula() const
{ {
@ -344,7 +338,6 @@ namespace spot
bool syntactic_si:1; // LTL-X or siPSL bool syntactic_si:1; // LTL-X or siPSL
bool sugar_free_ltl:1; // No F and G operators. bool sugar_free_ltl:1; // No F and G operators.
bool ltl_formula:1; // Only LTL operators. bool ltl_formula:1; // Only LTL operators.
bool eltl_formula:1; // Only ELTL operators.
bool psl_formula:1; // Only PSL operators. bool psl_formula:1; // Only PSL operators.
bool sere_formula:1; // Only SERE operators. bool sere_formula:1; // Only SERE operators.
bool finite:1; // Finite SERE formulae, or Bool+X forms. bool finite:1; // Finite SERE formulae, or Bool+X forms.

2
src/ltlast/multop.cc
View file

@ -60,7 +60,6 @@ namespace spot
// NOT Boolean. // NOT Boolean.
is.boolean = false; is.boolean = false;
is.ltl_formula = false; is.ltl_formula = false;
is.eltl_formula = false;
is.psl_formula = false; is.psl_formula = false;
is.eventual = false; is.eventual = false;
is.universal = false; is.universal = false;
@ -88,7 +87,6 @@ namespace spot
// and the result is therefore NOT Boolean. // and the result is therefore NOT Boolean.
is.boolean = false; is.boolean = false;
is.ltl_formula = false; is.ltl_formula = false;
is.eltl_formula = false;
is.psl_formula = false; is.psl_formula = false;
is.eventual = false; is.eventual = false;
is.universal = false; is.universal = false;

5
src/ltlast/unop.cc
View file

@ -59,7 +59,6 @@ namespace spot
is.not_marked = true; is.not_marked = true;
is.boolean = false; is.boolean = false;
is.syntactic_si = false; is.syntactic_si = false;
is.eltl_formula = false;
is.sere_formula = false; is.sere_formula = false;
// is.syntactic_safety inherited // is.syntactic_safety inherited
// is.syntactic_guarantee inherited // is.syntactic_guarantee inherited
@ -71,7 +70,6 @@ namespace spot
case F: case F:
is.not_marked = true; is.not_marked = true;
is.boolean = false; is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false; is.sere_formula = false;
is.finite = false; is.finite = false;
is.sugar_free_ltl = false; is.sugar_free_ltl = false;
@ -86,7 +84,6 @@ namespace spot
case G: case G:
is.not_marked = true; is.not_marked = true;
is.boolean = false; is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false; is.sere_formula = false;
is.finite = false; is.finite = false;
is.sugar_free_ltl = false; is.sugar_free_ltl = false;
@ -103,7 +100,6 @@ namespace spot
is.not_marked = (op == NegClosure); is.not_marked = (op == NegClosure);
is.boolean = false; is.boolean = false;
is.ltl_formula = false; is.ltl_formula = false;
is.eltl_formula = false;
is.psl_formula = true; is.psl_formula = true;
is.sere_formula = false; is.sere_formula = false;
is.syntactic_safety = is.finite; is.syntactic_safety = is.finite;
@ -119,7 +115,6 @@ namespace spot
is.not_marked = true; is.not_marked = true;
is.boolean = false; is.boolean = false;
is.ltl_formula = false; is.ltl_formula = false;
is.eltl_formula = false;
is.psl_formula = true; is.psl_formula = true;
is.sere_formula = false; is.sere_formula = false;
is.syntactic_safety = true; is.syntactic_safety = true;

12
src/tests/kind.test
View file

@ -26,10 +26,10 @@
set -e set -e
cat >input<<EOF cat >input<<EOF
a,B&!xfLEPSFsgopra a,B&!xfLPSFsgopra
a<->b,BxfLEPSFsgopra a<->b,BxfLPSFsgopra
!a,B&!xfLEPSFsgopra !a,B&!xfLPSFsgopra
!(a|b),B&xfLEPSFsgopra !(a|b),B&xfLPSFsgopra
F(a),&!xLPegopra F(a),&!xLPegopra
G(a),&!xLPusopra G(a),&!xLPusopra
a U b,&!xfLPgopra a U b,&!xfLPgopra
@ -95,8 +95,8 @@ Fa -> Gb,xLPsopra
{a;c|d;b}<>->GFb,&!Pra {a;c|d;b}<>->GFb,&!Pra
{a;c|d;_b}<>->!FGb,&Pr {a;c|d;_b}<>->!FGb,&Pr
# Equivalent to a&b&c&d # Equivalent to a&b&c&d
{a:b:c:d}!,B&!xfLEPSFsgopra {a:b:c:d}!,B&!xfLPSFsgopra
a&b&c&d,B&!xfLEPSFsgopra a&b&c&d,B&!xfLPSFsgopra
(Xa <-> XXXc) U (b & Fe),LPgopra (Xa <-> XXXc) U (b & Fe),LPgopra
(!X(a|X(!b))&(FX(g xor h)))U(!G(a|b)),LPegopra (!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 (!X(a|X(!b))&(GX(g xor h)))R(!F(a|b)),LPusopra