Commit 34f1601b authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

ltl: rename is_X_free() into is_syntactic_stutter_invariant()

and adjust it to detect siPSL formulas, as in the paper of Dax et
al. (ATVA'09).  For issue #51.

* 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: Rename
the property, and adjust its computation on siSERE.
* src/ltlvisit/remove_x.cc, src/ltlvisit/simplify.cc,
src/tgbaalgos/stutter.cc: Adjust to new names.
* src/bin/ltlfilt.cc: Add option --syntactic-sutter-invariant.
* src/ltltest/kind.test: Update tests and add some new.
parent a79db4ee
......@@ -58,7 +58,7 @@ Exit status:\n\
#define OPT_DROP_ERRORS 2
#define OPT_NNF 3
#define OPT_LTL 4
#define OPT_NOX 5
#define OPT_SYNTACTIC_SI 5
#define OPT_BOOLEAN 6
#define OPT_EVENTUAL 7
#define OPT_UNIVERSAL 8
......@@ -121,7 +121,6 @@ static const argp_option options[] =
{ 0, 0, 0, 0,
"Filtering options (matching is done after transformation):", 5 },
{ "ltl", OPT_LTL, 0, 0, "match only LTL formulas (no PSL operator)", 0 },
{ "nox", OPT_NOX, 0, 0, "match X-free formulas", 0 },
{ "boolean", OPT_BOOLEAN, 0, 0, "match Boolean formulas", 0 },
{ "eventual", OPT_EVENTUAL, 0, 0, "match pure eventualities", 0 },
{ "universal", OPT_UNIVERSAL, 0, 0, "match purely universal formulas", 0 },
......@@ -135,6 +134,9 @@ static const argp_option options[] =
"match syntactic-recurrence formulas", 0 },
{ "syntactic-persistence", OPT_SYNTACTIC_PERSISTENCE, 0, 0,
"match syntactic-persistence formulas", 0 },
{ "syntactic-stutter-invariant", OPT_SYNTACTIC_SI, 0, 0,
"match stutter-invariant formulas syntactically (LTL-X or siPSL)", 0 },
{ "nox", 0, 0, OPTION_ALIAS, 0, 0 },
{ "safety", OPT_SAFETY, 0, 0,
"match safety formulas (even pathological)", 0 },
{ "guarantee", OPT_GUARANTEE, 0, 0,
......@@ -206,7 +208,6 @@ static bool boolean_to_isop = false;
static bool unique = false;
static bool psl = false;
static bool ltl = false;
static bool nox = false;
static bool invert = false;
static bool boolean = false;
static bool universal = false;
......@@ -216,6 +217,7 @@ static bool syntactic_guarantee = false;
static bool syntactic_obligation = false;
static bool syntactic_recurrence = false;
static bool syntactic_persistence = false;
static bool syntactic_si = false;
static bool safety = false;
static bool guarantee = false;
static bool obligation = false;
......@@ -349,9 +351,6 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_NNF:
nnf = true;
break;
case OPT_NOX:
nox = true;
break;
case OPT_OBLIGATION:
obligation = true;
break;
......@@ -407,6 +406,9 @@ parse_opt(int key, char* arg, struct argp_state*)
case OPT_SYNTACTIC_PERSISTENCE:
syntactic_persistence = true;
break;
case OPT_SYNTACTIC_SI:
syntactic_si = true;
break;
case OPT_UNIVERSAL:
universal = true;
break;
......@@ -558,7 +560,6 @@ namespace
matched &= !ltl || f->is_ltl_formula();
matched &= !psl || f->is_psl_formula();
matched &= !nox || f->is_X_free();
matched &= !boolean || f->is_boolean();
matched &= !universal || f->is_universal();
matched &= !eventual || f->is_eventual();
......@@ -567,6 +568,7 @@ namespace
matched &= !syntactic_obligation || f->is_syntactic_obligation();
matched &= !syntactic_recurrence || f->is_syntactic_recurrence();
matched &= !syntactic_persistence || f->is_syntactic_persistence();
matched &= !syntactic_si || f->is_syntactic_stutter_invariant();
matched &= !ap || atomic_prop_collect(f)->size() == ap_n;
if (matched && (size_min > 0 || size_max >= 0))
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
......@@ -38,7 +38,10 @@ namespace spot
is.boolean = true;
is.sugar_free_boolean = true;
is.in_nenoform = true;
is.X_free = true;
is.syntactic_si = true; // Assuming LTL (for PSL a Boolean
// term is not stared will be regarded
// as not stuttering were this
// matters.)
is.sugar_free_ltl = true;
is.ltl_formula = true;
is.eltl_formula = true;
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
// de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
......@@ -132,6 +132,8 @@ namespace spot
}
assert(first->is_sere_formula());
assert(second->is_psl_formula());
if (first->is_boolean())
is.syntactic_si = false;
break;
case UConcat:
is.not_marked = true;
......@@ -158,6 +160,8 @@ namespace spot
}
assert(first->is_sere_formula());
assert(second->is_psl_formula());
if (first->is_boolean())
is.syntactic_si = false;
break;
case U:
is.not_marked = true;
......
......@@ -57,14 +57,28 @@ namespace spot
{
case Star:
if (max_ == unbounded)
is.finite = false;
{
is.finite = false;
is.syntactic_si = min_ == 1 && child->is_boolean();
}
else
{
is.syntactic_si = false;
}
if (min_ == 0)
is.accepting_eword = true;
break;
case FStar:
is.accepting_eword = false;
if (max_ == unbounded)
is.finite = false;
{
is.finite = false;
is.syntactic_si &= !child->is_boolean();
}
else
{
is.syntactic_si = false;
}
break;
}
}
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
// de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
......@@ -43,7 +43,7 @@ namespace spot
is.boolean = true;
is.sugar_free_boolean = true;
is.in_nenoform = true;
is.X_free = true;
is.syntactic_si = true; // for LTL (not PSL)
is.sugar_free_ltl = true;
is.ltl_formula = true;
is.eltl_formula = true;
......@@ -64,7 +64,7 @@ namespace spot
is.boolean = false;
is.sugar_free_boolean = false;
is.in_nenoform = true;
is.X_free = true;
is.syntactic_si = true;
is.sugar_free_ltl = true;
is.ltl_formula = false;
is.eltl_formula = false;
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
......@@ -39,7 +39,8 @@ namespace spot
proprint(is_boolean, "B", "Boolean formula"); \
proprint(is_sugar_free_boolean, "&", "without Boolean sugar"); \
proprint(is_in_nenoform, "!", "in negative normal form"); \
proprint(is_X_free, "x", "without X operator"); \
proprint(is_syntactic_stutter_invariant, "x", \
"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"); \
......
// -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire
// de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015
// Laboratoire de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
//
// This file is part of Spot, a model checking library.
......@@ -153,10 +153,10 @@ namespace spot
return is.in_nenoform;
}
/// Whether the formula avoids the X operator.
bool is_X_free() const
/// Whether the formula is syntactically stutter_invariant
bool is_syntactic_stutter_invariant() const
{
return is.X_free;
return is.syntactic_si;
}
/// Whether the formula avoids the F and G operators.
......@@ -337,7 +337,7 @@ namespace spot
bool boolean:1; // No temporal operators.
bool sugar_free_boolean:1; // Only AND, OR, and NOT operators.
bool in_nenoform:1; // Negative Normal Form.
bool X_free:1; // No X operators.
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.
......
......@@ -50,34 +50,61 @@ namespace spot
case Concat:
case AndNLM:
case AndRat:
// Note: AndNLM(p1,p2) and AndRat(p1,p2) are Boolean
// formulae, but there are actually rewritten as And(p1,p2)
// by trivial identities before this constructor is called.
// So at this point, AndNLM/AndRat are always used with at
// most one Boolean argument, 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;
{
bool syntactic_si = is.syntactic_si && !is.boolean;
// Note: AndNLM(p1,p2) and AndRat(p1,p2) are Boolean
// formulae, but they are actually rewritten as And(p1,p2)
// by trivial identities before this constructor is called.
// So at this point, AndNLM/AndRat are always used with at
// most one Boolean argument, 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;
for (unsigned i = 1; i < s; ++i)
{
syntactic_si &= (*v)[i]->is_syntactic_stutter_invariant()
&& !(*v)[i]->is_boolean();
props &= (*v)[i]->get_props();
}
is.syntactic_si = syntactic_si;
break;
}
case And:
for (unsigned i = 1; i < s; ++i)
props &= (*v)[i]->get_props();
break;
case OrRat:
// Note: OrRat(p1,p2) is a Boolean formula, but its is
// actually rewritten as Or(p1,p2) by trivial identities
// before this constructor is called. So at this point,
// AndNLM is always used with at most one Boolean argument,
// 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;
{
bool syntactic_si = is.syntactic_si && !is.boolean;
// Note: OrRat(p1,p2) is a Boolean formula, but its is
// actually rewritten as Or(p1,p2) by trivial identities
// before this constructor is called. So at this point,
// AndNLM is always used with at most one Boolean argument,
// 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;
bool ew = (*v)[0]->accepts_eword();
for (unsigned i = 1; i < s; ++i)
{
ew |= (*v)[i]->accepts_eword();
syntactic_si &= (*v)[i]->is_syntactic_stutter_invariant()
&& !(*v)[i]->is_boolean();
props &= (*v)[i]->get_props();
}
is.accepting_eword = ew;
is.syntactic_si = syntactic_si;
break;
}
case Or:
{
bool ew = (*v)[0]->accepts_eword();
......@@ -90,6 +117,32 @@ namespace spot
break;
}
}
// A concatenation is an siSERE if it contains one stared
// Boolean, and the other operands are siSERE (i.e.,
// sub-formulas that verify is_syntactic_stutter_invariant() and
// !is_boolean());
if (op == Concat)
{
unsigned sb = 0; // stared Boolean formulas seen
for (unsigned i = 0; i < s; ++i)
{
if ((*v)[i]->is_syntactic_stutter_invariant()
&& !(*v)[i]->is_boolean())
continue;
if (const bunop* b = is_Star((*v)[i]))
{
sb += b->child()->is_boolean();
if (sb > 1)
break;
}
else
{
sb = 0;
break;
}
}
is.syntactic_si = sb == 1;
}
}
multop::~multop()
......
// -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2015 Laboratoire
// de Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie.
......@@ -58,7 +58,7 @@ namespace spot
case X:
is.not_marked = true;
is.boolean = false;
is.X_free = false;
is.syntactic_si = false;
is.eltl_formula = false;
is.sere_formula = false;
// is.syntactic_safety inherited
......@@ -112,6 +112,8 @@ namespace spot
is.syntactic_recurrence = true;
is.syntactic_persistence = true;
is.accepting_eword = false;
assert(child->is_sere_formula());
assert(!child->is_boolean());
break;
case Closure:
is.not_marked = true;
......@@ -127,6 +129,7 @@ namespace spot
is.syntactic_persistence = true;
is.accepting_eword = false;
assert(child->is_sere_formula());
assert(!child->is_boolean());
break;
}
}
......
......@@ -59,32 +59,47 @@ check '(Ga|Fc) -> Fb' 'xLPopr'
check '(Ga|Fa) -> Gb' 'xLPopr'
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}|->!Fb' '&Psopr'
check '{a;c*;b}|->G!b' '&!Psopr'
check '{a;c*;b}|->!Gb' '&Pr'
check '{a;c*;b}|->F!b' '&!Pr'
check '{a;c*;b}|->GFa' '&!Pr'
check '{a;c*;b}|->FGa' '&!P'
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|(d;e)}|->!Xb' '&fPFsgopr'
check '{a;c;b|(d;e)}|->X!b' '&!fPFsgopr'
check '{a;c;b|(d;e)}|->!Fb' '&xPsopr'
check '{a;c;b|(d;e)}|->G!b' '&!xPsopr'
check '{a;c;b|(d;e)}|->!Gb' '&xPgopr'
check '{a;c;b|(d;e)}|->F!b' '&!xPgopr'
check '{a;c;b|(d;e)}|->GFa' '&!xPr'
check '{a;c;b|(d;e)}|->FGa' '&!xPp'
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;c*;b}<>->GFb' '&!xP'
check '{a;c*;b}<>->!FGb' '&xP'
check '{a;c|d;b}<>->!Gb' '&xPgopr'
check '{a;c|d;b}<>->G!b' '&!xPsopr'
check '{a;c|d;b}<>->FGb' '&!xPp'
check '{a;c|d;b}<>->!GFb' '&xPp'
check '{a;c|d;b}<>->GFb' '&!xPr'
check '{a;c|d;b}<>->!FGb' '&xPr'
check '{a;c;b|(d;e)}|->!Fb' '&Psopr'
check '{a;c;b|(d;e)}|->G!b' '&!Psopr'
check '{a;c;b|(d;e)}|->!Gb' '&Pgopr'
check '{a;c;b|(d;e)}|->F!b' '&!Pgopr'
check '{a;c;b|(d;e)}|->GFa' '&!Pr'
check '{a;c;b|(d;e)}|->FGa' '&!Pp'
check '{a[+] && c[+]}|->!Xb' '&fPsopr'
check '{a[+] && c[+]}|->X!b' '&!fPsopr'
check '{a[+] && c[+]}|->!Fb' '&xPsopr'
check '{a[+] && c[+]}|->G!b' '&!xPsopr'
check '{a[+] && c[+]}|->!Gb' '&xPr'
check '{a[+] && c[+]}|->F!b' '&!xPr'
check '{a[+] && c[+]}|->GFa' '&!xPr'
check '{a[+] && c[+]}|->FGa' '&!xP'
check '{a;c*;b}<>->!Gb' '&Pgopr'
check '{a;c*;b}<>->F!b' '&!Pgopr'
check '{a;c*;b}<>->FGb' '&!Pp'
check '{a;c*;b}<>->!GFb' '&Pp'
check '{a;c*;b}<>->GFb' '&!P'
check '{a;c*;b}<>->!FGb' '&P'
check '{a*;c[+];b[+]}<>->!FGb' '&xP'
check '{a;c|d;b}<>->!Gb' '&Pgopr'
check '{a;c|d;b}<>->G!b' '&!Psopr'
check '{a;c|d;b}<>->FGb' '&!Pp'
check '{a;c|d;b}<>->!GFb' '&Pp'
check '{a;c|d;b}<>->GFb' '&!Pr'
check '{a;c|d;b}<>->!FGb' '&Pr'
check '{a:b:c:d}!' 'B&!xfLEPSFsgopr' # Equivalent to a&b&c&d
check 'a&b&c&d' 'B&!xfLEPSFsgopr'
check '(Xa <-> XXXc) U (b & Fe)' 'LPgopr'
......@@ -110,11 +125,15 @@ check 'FGa W FGb' '&!xLPeu'
check 'Ga W FGb' '&!xLPup'
check 'Ga W b' '&!xLPsopr'
check 'Fa M b' '&!xLPgopr'
check '{a;b*;c}' '&!xfPsopr'
check '{a;b*;c}!' '&!xfPgopr'
check '!{a;b*;c}!' '&xfPsopr' # The negative normal form is {a;b*;c}[]->0
check '{a;b*;c}[]->0' '&!xfPsopr'
check '!{a;b*;c}' '&!xfPgopr'
check '{a;b*;c}' '&!fPsopr'
check '{a;b*;c}!' '&!fPgopr'
check '!{a;b*;c}!' '&fPsopr' # The negative normal form is {a;b*;c}[]->0
check '{a;b*;c}[]->0' '&!fPsopr'
check '!{a;b*;c}' '&!fPgopr'
check '!{a[+];b*;c[+]}' '&!xfPgopr'
check '{a[+];b*;c[+]}' '&!xfPsopr'
check '{a[+] && b || c[+]}' '&!fPsopr'
check '{a[+] && b[+] || c[+]}' '&!xfPsopr'
run 0 ../consterm '1'
run 0 ../consterm '0'
......
......@@ -104,7 +104,7 @@ namespace spot
virtual const formula* recurse(const formula* f)
{
if (f->is_X_free())
if (f->is_syntactic_stutter_invariant())
return f->clone();
f->accept(*this);
return this->result();
......
......@@ -2805,7 +2805,7 @@ namespace spot
// a & (Xa U b) = b M a
// a & (b | X(b R a)) = b R a
// a & (b | X(b M a)) = b M a
if (!mo->is_X_free())
if (!mo->is_syntactic_stutter_invariant()) // Skip if no X.
{
typedef std::unordered_set<const formula*,
ptr_hash<formula>> fset_t;
......@@ -2825,7 +2825,7 @@ namespace spot
{
if (!(*res)[n])
continue;
if ((*res)[n]->is_X_free())
if ((*res)[n]->is_syntactic_stutter_invariant())
continue;
const formula* xarg = is_XWU((*res)[n]);
......@@ -3530,7 +3530,7 @@ namespace spot
// a | (Xa M b) = b U a
// a | (b & X(b W a)) = b W a
// a | (b & X(b U a)) = b U a
if (!mo->is_X_free())
if (!mo->is_syntactic_stutter_invariant()) // Skip if no X
{
typedef std::unordered_set<const formula*,
ptr_hash<formula>> fset_t;
......@@ -3551,7 +3551,7 @@ namespace spot
{
if (!(*res)[n])
continue;
if ((*res)[n]->is_X_free())
if ((*res)[n]->is_syntactic_stutter_invariant())
continue;
const formula* xarg = is_XRM((*res)[n]);
......
......@@ -517,7 +517,7 @@ namespace spot
bool
is_stutter_invariant(const ltl::formula* f)
{
if (f->is_ltl_formula() && f->is_X_free())
if (f->is_ltl_formula() && f->is_syntactic_stutter_invariant())
return true;
int algo = default_stutter_check_algorithm();
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment