Track syntactic classes.
These are safety, guarantee, obligation, persistence, and recurrence. * src/ltlast/formula.hh, src/ltlast/formula.cc: Declare a bit for each of these classes. * src/ltlast/atomic_prop.cc, src/ltlast/constant.cc, src/ltlast/automatop.cc, src/ltlast/binop.cc, src/ltlast/bunop.cc, src/ltlast/unop.cc: Update these bits. * src/ltltest/kind.test: Update tests and add more.
This commit is contained in:
Alexandre Duret-Lutz
parent
2669df1c96
commit
df760a4597
9 changed files with 273 additions and 24 deletions
|
|
@ -45,6 +45,11 @@ namespace spot
|
|||
is.sere_formula = true;
|
||||
is.eventual = false;
|
||||
is.universal = false;
|
||||
is.syntactic_safety = true;
|
||||
is.syntactic_guarantee = true;
|
||||
is.syntactic_obligation = true;
|
||||
is.syntactic_recurrence = true;
|
||||
is.syntactic_persistence = true;
|
||||
is.not_marked = true;
|
||||
is.accepting_eword = false;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -41,6 +41,11 @@ namespace spot
|
|||
is.sere_formula = false;
|
||||
is.eventual = false;
|
||||
is.universal = false;
|
||||
is.syntactic_safety = false;
|
||||
is.syntactic_guarantee = false;
|
||||
is.syntactic_obligation = false;
|
||||
is.syntactic_recurrence = false;
|
||||
is.syntactic_persistence = false;
|
||||
is.not_marked = true;
|
||||
is.accepting_eword = false;
|
||||
|
||||
|
|
|
|||
|
|
@ -53,17 +53,69 @@ namespace spot
|
|||
switch (op)
|
||||
{
|
||||
case Xor:
|
||||
case Implies:
|
||||
case Equiv:
|
||||
is.sere_formula = is.boolean;
|
||||
is.sugar_free_boolean = false;
|
||||
is.in_nenoform = false;
|
||||
// is.syntactic_obligation inherited;
|
||||
is.accepting_eword = false;
|
||||
if (is.syntactic_obligation)
|
||||
{
|
||||
// Only formula that are in the intersection of
|
||||
// guarantee and safety are closed by Xor and <=>.
|
||||
bool sg = is.syntactic_safety && is.syntactic_guarantee;
|
||||
bool rp = is.syntactic_recurrence && is.syntactic_persistence;
|
||||
is.syntactic_safety = sg;
|
||||
is.syntactic_guarantee = sg;
|
||||
is.syntactic_recurrence = rp;
|
||||
is.syntactic_persistence = rp;
|
||||
}
|
||||
else
|
||||
{
|
||||
is.syntactic_safety = false;
|
||||
is.syntactic_guarantee = false;
|
||||
}
|
||||
break;
|
||||
case Implies:
|
||||
is.sere_formula = is.boolean;
|
||||
is.sugar_free_boolean = false;
|
||||
is.in_nenoform = false;
|
||||
is.syntactic_safety =
|
||||
first->is_syntactic_obligation() && second->is_syntactic_safety();
|
||||
is.syntactic_obligation =
|
||||
first->is_syntactic_safety() && second->is_syntactic_obligation();
|
||||
// is.syntactic_obligation inherited
|
||||
is.syntactic_persistence = first->is_syntactic_recurrence()
|
||||
&& second->is_syntactic_persistence();
|
||||
is.syntactic_recurrence = first->is_syntactic_persistence()
|
||||
&& second->is_syntactic_recurrence();
|
||||
is.accepting_eword = false;
|
||||
break;
|
||||
case EConcatMarked:
|
||||
is.not_marked = false;
|
||||
// fall through
|
||||
case EConcat:
|
||||
is.ltl_formula = false;
|
||||
is.boolean = false;
|
||||
is.eltl_formula = false;
|
||||
is.sere_formula = false;
|
||||
is.accepting_eword = false;
|
||||
is.psl_formula = true;
|
||||
|
||||
// FIXME: if we know that the SERE has a finite language.
|
||||
// (i.e. no star). Then
|
||||
// is.syntactic_safety = second->is_syntactic_safety();
|
||||
// is.syntactic_obligation = second->is_syntactic_obligation();
|
||||
// is.syntactic_recurrence = second->is_syntactic_recurrence();
|
||||
is.syntactic_safety = false;
|
||||
is.syntactic_guarantee = second->is_syntactic_guarantee();
|
||||
is.syntactic_obligation = second->is_syntactic_guarantee();
|
||||
is.syntactic_recurrence = second->is_syntactic_guarantee();
|
||||
is.syntactic_persistence = second->is_syntactic_persistence();
|
||||
|
||||
assert(first->is_sere_formula());
|
||||
assert(second->is_psl_formula());
|
||||
break;
|
||||
case UConcat:
|
||||
is.ltl_formula = false;
|
||||
is.boolean = false;
|
||||
|
|
@ -71,6 +123,18 @@ namespace spot
|
|||
is.sere_formula = false;
|
||||
is.accepting_eword = false;
|
||||
is.psl_formula = true;
|
||||
|
||||
// FIXME: if we know that the SERE has a finite language.
|
||||
// (i.e. no star). Then
|
||||
// is.syntactic_guarantee = second->is_syntactic_guarantee();
|
||||
// is.syntactic_obligation = second->is_syntactic_obligation();
|
||||
// is.syntactic_persistence = second->is_syntactic_persistence();
|
||||
is.syntactic_safety = second->is_syntactic_safety();
|
||||
is.syntactic_guarantee = false;
|
||||
is.syntactic_obligation = second->is_syntactic_safety();
|
||||
is.syntactic_recurrence = second->is_syntactic_recurrence();
|
||||
is.syntactic_persistence = second->is_syntactic_safety();
|
||||
|
||||
assert(first->is_sere_formula());
|
||||
assert(second->is_psl_formula());
|
||||
break;
|
||||
|
|
@ -82,6 +146,16 @@ namespace spot
|
|||
is.eltl_formula = false;
|
||||
is.sere_formula = false;
|
||||
is.accepting_eword = false;
|
||||
|
||||
is.syntactic_safety = false;
|
||||
// is.syntactic_guarantee = Guarantee U Guarantee
|
||||
is.syntactic_obligation = // Obligation U Guarantee
|
||||
first->is_syntactic_obligation()
|
||||
&& second->is_syntactic_guarantee();
|
||||
is.syntactic_recurrence = // Recurrence U Guarantee
|
||||
first->is_syntactic_recurrence()
|
||||
&& second->is_syntactic_guarantee();
|
||||
// is.syntactic_persistence = Persistence U Persistance
|
||||
break;
|
||||
case W:
|
||||
// a W 0 = Ga
|
||||
|
|
@ -91,6 +165,16 @@ namespace spot
|
|||
is.eltl_formula = false;
|
||||
is.sere_formula = false;
|
||||
is.accepting_eword = false;
|
||||
|
||||
// is.syntactic_safety = Safety W Safety;
|
||||
is.syntactic_guarantee = false;
|
||||
is.syntactic_obligation = // Safety W Obligation
|
||||
first->is_syntactic_safety() && second->is_syntactic_obligation();
|
||||
// is.syntactic_recurrence = Recurrence W Recurrence
|
||||
is.syntactic_persistence = // Safety W Persistance
|
||||
first->is_syntactic_safety()
|
||||
&& second->is_syntactic_persistence();
|
||||
|
||||
break;
|
||||
case R:
|
||||
// 0 R a = Ga
|
||||
|
|
@ -100,6 +184,16 @@ namespace spot
|
|||
is.eltl_formula = false;
|
||||
is.sere_formula = false;
|
||||
is.accepting_eword = false;
|
||||
|
||||
// is.syntactic_safety = Safety R Safety;
|
||||
is.syntactic_guarantee = false;
|
||||
is.syntactic_obligation = // Obligation R Safety
|
||||
first->is_syntactic_obligation() && second->is_syntactic_safety();
|
||||
//is.syntactic_recurrence = Recurrence R Recurrence
|
||||
is.syntactic_persistence = // Persistence R Safety
|
||||
first->is_syntactic_persistence()
|
||||
&& second->is_syntactic_safety();
|
||||
|
||||
break;
|
||||
case M:
|
||||
// a M 1 = Fa
|
||||
|
|
@ -109,8 +203,22 @@ namespace spot
|
|||
is.eltl_formula = false;
|
||||
is.sere_formula = false;
|
||||
is.accepting_eword = false;
|
||||
|
||||
is.syntactic_safety = false;
|
||||
// is.syntactic_guarantee = Guarantee M Guarantee
|
||||
is.syntactic_obligation = // Guarantee M Obligation
|
||||
first->is_syntactic_guarantee()
|
||||
&& second->is_syntactic_obligation();
|
||||
is.syntactic_recurrence = // Guarantee M Recurrence
|
||||
first->is_syntactic_guarantee()
|
||||
&& second->is_syntactic_recurrence();
|
||||
// is.syntactic_persistence = Persistence M Persistance
|
||||
|
||||
break;
|
||||
}
|
||||
|
||||
assert((!is.syntactic_obligation) ||
|
||||
(is.syntactic_persistence && is.syntactic_recurrence));
|
||||
}
|
||||
|
||||
binop::~binop()
|
||||
|
|
|
|||
|
|
@ -42,6 +42,11 @@ namespace spot
|
|||
is.psl_formula = false;
|
||||
is.eventual = false;
|
||||
is.universal = false;
|
||||
is.syntactic_safety = false;
|
||||
is.syntactic_guarantee = false;
|
||||
is.syntactic_obligation = false;
|
||||
is.syntactic_recurrence = false;
|
||||
is.syntactic_persistence = false;
|
||||
|
||||
switch (op_)
|
||||
{
|
||||
|
|
|
|||
|
|
@ -51,6 +51,11 @@ namespace spot
|
|||
is.sere_formula = true;
|
||||
is.eventual = true;
|
||||
is.universal = true;
|
||||
is.syntactic_safety = true;
|
||||
is.syntactic_guarantee = true;
|
||||
is.syntactic_obligation = true;
|
||||
is.syntactic_recurrence = true;
|
||||
is.syntactic_persistence = true;
|
||||
is.not_marked = true;
|
||||
is.accepting_eword = false;
|
||||
break;
|
||||
|
|
@ -65,6 +70,11 @@ namespace spot
|
|||
is.psl_formula = false;
|
||||
is.sere_formula = true;
|
||||
is.eventual = false;
|
||||
is.syntactic_safety = false;
|
||||
is.syntactic_guarantee = false;
|
||||
is.syntactic_obligation = false;
|
||||
is.syntactic_recurrence = false;
|
||||
is.syntactic_persistence = false;
|
||||
is.universal = false;
|
||||
is.not_marked = true;
|
||||
is.accepting_eword = true;
|
||||
|
|
|
|||
|
|
@ -86,6 +86,11 @@ namespace spot
|
|||
proprint(is_sere_formula, "S", "SERE formula");
|
||||
proprint(is_eventual, "e", "pure eventuality");
|
||||
proprint(is_universal, "u", "purely universal");
|
||||
proprint(is_syntactic_safety, "s", "syntactic safety");
|
||||
proprint(is_syntactic_guarantee, "g", "syntactic guarantee");
|
||||
proprint(is_syntactic_obligation, "o", "syntactic obligation");
|
||||
proprint(is_syntactic_persistence, "p", "syntactic persistence");
|
||||
proprint(is_syntactic_recurrence, "r", "syntactic recurrence");
|
||||
proprint(is_marked, "+", "marked");
|
||||
proprint(accepts_eword, "0", "accepts the empty word");
|
||||
return out;
|
||||
|
|
|
|||
|
|
@ -226,6 +226,36 @@ namespace spot
|
|||
return is.universal;
|
||||
}
|
||||
|
||||
/// Whether a PSL/LTL formula is syntactic safety property.
|
||||
bool is_syntactic_safety() const
|
||||
{
|
||||
return is.syntactic_safety;
|
||||
}
|
||||
|
||||
/// Whether a PSL/LTL formula is syntactic guarantee property.
|
||||
bool is_syntactic_guarantee() const
|
||||
{
|
||||
return is.syntactic_guarantee;
|
||||
}
|
||||
|
||||
/// Whether a PSL/LTL formula is syntactic obligation property.
|
||||
bool is_syntactic_obligation() const
|
||||
{
|
||||
return is.syntactic_obligation;
|
||||
}
|
||||
|
||||
/// Whether a PSL/LTL formula is syntactic recurrence property.
|
||||
bool is_syntactic_recurrence() const
|
||||
{
|
||||
return is.syntactic_recurrence;
|
||||
}
|
||||
|
||||
/// Whether a PSL/LTL formula is syntactic persistence property.
|
||||
bool is_syntactic_persistence() const
|
||||
{
|
||||
return is.syntactic_persistence;
|
||||
}
|
||||
|
||||
/// Whether the formula has an occurrence of EConcatMarked.
|
||||
bool is_marked() const
|
||||
{
|
||||
|
|
@ -288,6 +318,11 @@ namespace spot
|
|||
bool sere_formula:1; // Only SERE operators.
|
||||
bool eventual:1; // Purely eventual formula.
|
||||
bool universal:1; // Purely universal formula.
|
||||
bool syntactic_safety:1; // Syntactic Safety Property.
|
||||
bool syntactic_guarantee:1; // Syntactic Guarantee Property.
|
||||
bool syntactic_obligation:1; // Syntactic Obligation Property.
|
||||
bool syntactic_recurrence:1; // Syntactic Recurrence Property.
|
||||
bool syntactic_persistence:1; // Syntactic Persistence Property.
|
||||
bool not_marked:1; // No occurrence of EConcatMarked.
|
||||
bool accepting_eword:1; // Accepts the empty word.
|
||||
};
|
||||
|
|
|
|||
|
|
@ -41,6 +41,13 @@ namespace spot
|
|||
case Not:
|
||||
is.in_nenoform = (child->kind() == AtomicProp);
|
||||
is.sere_formula = is.boolean;
|
||||
|
||||
is.syntactic_safety = child->is_syntactic_guarantee();
|
||||
is.syntactic_guarantee = child->is_syntactic_safety();
|
||||
// is.syntactic_obligation inherited from child
|
||||
is.syntactic_recurrence = child->is_syntactic_persistence();
|
||||
is.syntactic_persistence = child->is_syntactic_recurrence();
|
||||
|
||||
is.accepting_eword = false;
|
||||
break;
|
||||
case X:
|
||||
|
|
@ -48,6 +55,11 @@ namespace spot
|
|||
is.X_free = false;
|
||||
is.eltl_formula = false;
|
||||
is.sere_formula = false;
|
||||
// is.syntactic_safety inherited
|
||||
// is.syntactic_guarantee inherited
|
||||
// is.syntactic_obligation inherited
|
||||
// is.syntactic_recurrence inherited
|
||||
// is.syntactic_persistence inherited
|
||||
is.accepting_eword = false;
|
||||
break;
|
||||
case F:
|
||||
|
|
@ -56,6 +68,11 @@ namespace spot
|
|||
is.sere_formula = false;
|
||||
is.sugar_free_ltl = false;
|
||||
is.eventual = true;
|
||||
is.syntactic_safety = false;
|
||||
// is.syntactic_guarantee inherited
|
||||
is.syntactic_obligation = is.syntactic_guarantee;
|
||||
is.syntactic_recurrence = is.syntactic_guarantee;
|
||||
// is.syntactic_persistence inherited
|
||||
is.accepting_eword = false;
|
||||
break;
|
||||
case G:
|
||||
|
|
@ -64,6 +81,11 @@ namespace spot
|
|||
is.sere_formula = false;
|
||||
is.sugar_free_ltl = false;
|
||||
is.universal = true;
|
||||
// is.syntactic_safety inherited
|
||||
is.syntactic_guarantee = false;
|
||||
is.syntactic_obligation = is.syntactic_safety;
|
||||
// is.syntactic_recurrence inherited
|
||||
is.syntactic_persistence = is.syntactic_safety;
|
||||
is.accepting_eword = false;
|
||||
break;
|
||||
case Finish:
|
||||
|
|
@ -71,17 +93,38 @@ namespace spot
|
|||
is.ltl_formula = false;
|
||||
is.psl_formula = false;
|
||||
is.sere_formula = false;
|
||||
is.syntactic_safety = false;
|
||||
is.syntactic_guarantee = false;
|
||||
is.syntactic_obligation = false;
|
||||
is.syntactic_recurrence = false;
|
||||
is.syntactic_persistence = false;
|
||||
is.accepting_eword = false;
|
||||
break;
|
||||
case NegClosure:
|
||||
is.not_marked = false;
|
||||
// fall through
|
||||
is.boolean = false;
|
||||
is.ltl_formula = false;
|
||||
is.eltl_formula = false;
|
||||
is.psl_formula = true;
|
||||
is.sere_formula = false;
|
||||
is.syntactic_safety = true;
|
||||
is.syntactic_guarantee = true;
|
||||
is.syntactic_obligation = true;
|
||||
is.syntactic_recurrence = true;
|
||||
is.syntactic_persistence = true;
|
||||
is.accepting_eword = false;
|
||||
break;
|
||||
case Closure:
|
||||
is.boolean = false;
|
||||
is.ltl_formula = false;
|
||||
is.eltl_formula = false;
|
||||
is.psl_formula = true;
|
||||
is.sere_formula = false;
|
||||
is.syntactic_safety = true;
|
||||
is.syntactic_guarantee = true;
|
||||
is.syntactic_obligation = true;
|
||||
is.syntactic_recurrence = true;
|
||||
is.syntactic_persistence = true;
|
||||
is.accepting_eword = false;
|
||||
assert(child->is_sere_formula());
|
||||
break;
|
||||
|
|
|
|||
|
|
@ -33,28 +33,61 @@ check()
|
|||
test "$word" = "$2"
|
||||
}
|
||||
|
||||
check 'a' 'B&!xfLEPS'
|
||||
check 'a<->b' 'BxfLEPS'
|
||||
check '!a' 'B&!xfLEPS'
|
||||
check '!(a|b)' 'B&xfLEPS'
|
||||
check 'F(a)' '&!xLPe'
|
||||
check 'G(a)' '&!xLPu'
|
||||
check 'a U b' '&!xfLP'
|
||||
check 'a U Fb' '&!xLP'
|
||||
check 'Ga U b' '&!xLP'
|
||||
check '1 U a' '&!xfLPe'
|
||||
check 'a W b' '&!xfLP'
|
||||
check 'a W 0' '&!xfLPu'
|
||||
check 'a M b' '&!xfLP'
|
||||
check 'a M 1' '&!xfLPe'
|
||||
check 'a R b' '&!xfLP'
|
||||
check '0 R b' '&!xfLPu'
|
||||
check '{a;b}|->!Xb' '&fP'
|
||||
check '{a;b}|->X!b' '&!fP'
|
||||
check '{a;b}|->!Gb' '&xP'
|
||||
check '{a;b}|->F!b' '&!xP'
|
||||
check '{a:b:c:d}!' 'B&!xfLEPS' # Equivalent to a&b&c&d
|
||||
check 'a&b&c&d' 'B&!xfLEPS'
|
||||
check 'a' 'B&!xfLEPSsgopr'
|
||||
check 'a<->b' 'BxfLEPSsgopr'
|
||||
check '!a' 'B&!xfLEPSsgopr'
|
||||
check '!(a|b)' 'B&xfLEPSsgopr'
|
||||
check 'F(a)' '&!xLPegopr'
|
||||
check 'G(a)' '&!xLPusopr'
|
||||
check 'a U b' '&!xfLPgopr'
|
||||
check 'a U Fb' '&!xLPgopr'
|
||||
check 'Ga U b' '&!xLPopr'
|
||||
check '1 U a' '&!xfLPegopr'
|
||||
check 'a W b' '&!xfLPsopr'
|
||||
check 'a W 0' '&!xfLPusopr'
|
||||
check 'a M b' '&!xfLPgopr'
|
||||
check 'a M 1' '&!xfLPegopr'
|
||||
check 'a R b' '&!xfLPsopr'
|
||||
check '0 R b' '&!xfLPusopr'
|
||||
check 'a R (b R (c R d))' '&!xfLPsopr'
|
||||
check 'a U (b U (c U d))' '&!xfLPgopr'
|
||||
check 'a W (b W (c W d))' '&!xfLPsopr'
|
||||
check 'a M (b M (c M d))' '&!xfLPgopr'
|
||||
check '{a;c*;b}|->!Xb' '&fPsopr'
|
||||
check '{a;c*;b}|->X!b' '&!fPsopr'
|
||||
check '{a;c*;b}|->!Fb' '&xPsopr'
|
||||
check '{a;c*;b}|->G!b' '&!xPsopr'
|
||||
check '{a;c*;b}|->!Gb' '&xPr'
|
||||
check '{a;c*;b}|->F!b' '&!xPr'
|
||||
check '{a;c*;b}|->GFa' '&!xPr'
|
||||
check '{a;c*;b}|->FGa' '&!xP'
|
||||
check '{a;c*;b}<>->!Gb' '&xPgopr'
|
||||
check '{a;c*;b}<>->F!b' '&!xPgopr'
|
||||
check '{a;c*;b}<>->FGb' '&!xPp'
|
||||
check '{a;c*;b}<>->!GFb' '&xPp'
|
||||
check '{a:b:c:d}!' 'B&!xfLEPSsgopr' # Equivalent to a&b&c&d
|
||||
check 'a&b&c&d' 'B&!xfLEPSsgopr'
|
||||
check '(Xa <-> XXXc) U (b & Fe)' 'LPgopr'
|
||||
check '(!X(a|X(!b))&(FX(g xor h)))U(!G(a|b))' 'LPgopr'
|
||||
check '(!X(a|X(!b))&(GX(g xor h)))R(!F(a|b))' 'LPsopr'
|
||||
check '(!X(a|X(!b))&(GX(g xor h)))U(!G(a|b))' 'LPopr'
|
||||
check '(!X(a|X(!b))&(FX(g xor h)))R(!F(a|b))' 'LPopr'
|
||||
check '(!X(a|X(!b))&(GX(g xor h)))U(!F(a|b))' 'LPp'
|
||||
check '(!X(a|X(!b))&(FX(g xor h)))R(!G(a|b))' 'LPr'
|
||||
check '(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|b))' 'LPp'
|
||||
check '(!X(a|GXF(!b))&(FGX(g xor h)))R(!F(a|b))' 'LPp'
|
||||
check '(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|b))' 'LPr'
|
||||
check '(!X(a|FXG(!b))&(GFX(g xor h)))U(!G(a|b))' 'LPr'
|
||||
check '(!X(a|GXF(!b))&(FGX(g xor h)))U(!G(a|Fb))' 'LPp'
|
||||
check '(!X(a|GXF(!b))&(FGX(g xor h)))U(!F(a|Gb))' 'LP'
|
||||
check '(!X(a|FXG(!b))&(GFX(g xor h)))R(!F(a|Gb))' 'LPr'
|
||||
check '(!X(a|FXG(!b))&(GFX(g xor h)))R(!G(a|Fb))' 'LP'
|
||||
check 'GFa M GFb' '&!xLPeu'
|
||||
check 'FGa M FGb' '&!xLPeup'
|
||||
check 'Fa M GFb' '&!xLPer'
|
||||
check 'GFa W GFb' '&!xLPeur'
|
||||
check 'FGa W FGb' '&!xLPeu'
|
||||
check 'Ga W FGb' '&!xLPup'
|
||||
|
||||
run 0 ../consterm '1'
|
||||
run 0 ../consterm '0'
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue