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

Track SERE formulas.

Browse source 
* src/ltlast/atomic_prop.cc, src/ltlast/automatop.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: Add a bit is.sere_formula
to track SEREs, and fix tracking of PSL formulae.
* src/ltltest/kind.test: Adjust.
This commit is contained in:
Alexandre Duret-Lutz 2011-02-20 17:08:39 +01:00
parent fdd73d5123
commit 459921ef60
10 changed files with 50 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/ltlast/atomic_prop.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010, 2011 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),
@ -42,6 +42,7 @@ namespace spot
is.ltl_formula = true;
is.eltl_formula = true;
is.psl_formula = true;
is.sere_formula = true;
is.eventual = false;
is.universal = false;
is.not_marked = true;

5
src/ltlast/automatop.cc
View file

@ -1,5 +1,5 @@
// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et Developpement
// de l'Epita (LRDE)
// Copyright (C) 2008, 2009, 2010, 2011 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE)
//
// This file is part of Spot, a model checking library.
//
@ -38,6 +38,7 @@ namespace spot
is.ltl_formula = false;
is.eltl_formula = true;
is.psl_formula = false;
is.sere_formula = false;
is.eventual = false;
is.universal = false;
is.not_marked = true;

11
src/ltlast/binop.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010, 2011 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),
@ -54,6 +54,7 @@ namespace spot
case Xor:
case Implies:
case Equiv:
is.sere_formula = is.boolean;
is.sugar_free_boolean = false;
is.in_nenoform = false;
is.accepting_eword = false;
@ -66,7 +67,11 @@ namespace spot
is.ltl_formula = false;
is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false;
is.accepting_eword = false;
is.psl_formula = true;
assert(first->is_sere_formula());
assert(second->is_psl_formula());
break;
case U:
// 1 U a = Fa
@ -74,6 +79,7 @@ namespace spot
is.eventual = 1;
is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false;
is.accepting_eword = false;
break;
case W:
@ -82,6 +88,7 @@ namespace spot
is.universal = 1;
is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false;
is.accepting_eword = false;
break;
case R:
@ -90,6 +97,7 @@ namespace spot
is.universal = 1;
is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false;
is.accepting_eword = false;
break;
case M:
@ -98,6 +106,7 @@ namespace spot
is.eventual = 1;
is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false;
is.accepting_eword = false;
break;
}

2
src/ltlast/bunop.cc
View file

@ -35,9 +35,11 @@ namespace spot
{
props = child->get_props();
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;

6
src/ltlast/constant.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et D<>veloppement
// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et D<>veloppement
// de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), d<>partement Syst<73>mes R<>partis Coop<6F>ratifs (SRC),
@ -48,6 +48,7 @@ namespace spot
is.ltl_formula = true;
is.eltl_formula = true;
is.psl_formula = true;
is.sere_formula = true;
is.eventual = true;
is.universal = true;
is.not_marked = true;
@ -61,7 +62,8 @@ namespace spot
is.sugar_free_ltl = true;
is.ltl_formula = false;
is.eltl_formula = false;
is.psl_formula = true;
is.psl_formula = false;
is.sere_formula = true;
is.eventual = false;
is.universal = false;
is.not_marked = true;

3
src/ltlast/formula.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010, 2011 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
@ -83,6 +83,7 @@ namespace spot
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_eventual, "e", "pure eventuality");
proprint(is_universal, "u", "purely universal");
proprint(is_marked, "+", "marked");

11
src/ltlast/formula.hh
View file

@ -1,5 +1,5 @@
// Copyright (C) 2008, 2009, 2010 Laboratoire de Recherche et D<>veloppement
// de l'Epita (LRDE).
// Copyright (C) 2008, 2009, 2010, 2011 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.
@ -170,6 +170,12 @@ namespace spot
return is.psl_formula;
}
/// Whether the formula use only SERE operators.
bool is_sere_formula() const
{
return is.sere_formula;
}
/// \brief Whether the formula is purely eventual.
///
/// Pure eventuality formulae are defined in
@ -279,6 +285,7 @@ namespace spot
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 eventual:1; // Purely eventual formula.
bool universal:1; // Purely universal formula.
bool not_marked:1; // No occurrence of EConcatMarked.

7
src/ltlast/multop.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et D<>veloppement
// Copyright (C) 2009, 2010, 2011 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),
@ -39,6 +39,8 @@ namespace spot
unsigned s = v->size();
assert(s > 1);
props = (*v)[0]->get_props();
switch (op)
{
case Concat:
@ -46,6 +48,7 @@ namespace spot
is.boolean = false;
is.ltl_formula = false;
is.eltl_formula = false;
is.psl_formula = false;
is.eventual = false;
is.universal = false;
// fall through
@ -55,14 +58,12 @@ namespace spot
// Boolean flag, because applied to atomic propositions a&b
// has the same effect as a&&b.
case And:
props = (*v)[0]->get_props();
for (unsigned i = 1; i < s; ++i)
props &= (*v)[i]->get_props();
break;
case Or:
{
bool ew = (*v)[0]->accepts_eword();
props = (*v)[0]->get_props();
for (unsigned i = 1; i < s; ++i)
{
ew |= (*v)[i]->accepts_eword();

10
src/ltlast/unop.cc
View file

@ -1,4 +1,4 @@
// Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement
// Copyright (C) 2009, 2010, 2011 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),
@ -40,17 +40,20 @@ namespace spot
{
case Not:
is.in_nenoform = (child->kind() == AtomicProp);
is.sere_formula = is.boolean;
is.accepting_eword = false;
break;
case X:
is.boolean = false;
is.X_free = false;
is.eltl_formula = false;
is.sere_formula = false;
is.accepting_eword = false;
break;
case F:
is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false;
is.sugar_free_ltl = false;
is.eventual = true;
is.accepting_eword = false;
@ -58,6 +61,7 @@ namespace spot
case G:
is.boolean = false;
is.eltl_formula = false;
is.sere_formula = false;
is.sugar_free_ltl = false;
is.universal = true;
is.accepting_eword = false;
@ -66,6 +70,7 @@ namespace spot
is.boolean = false;
is.ltl_formula = false;
is.psl_formula = false;
is.sere_formula = false;
is.accepting_eword = false;
break;
case NegClosure:
@ -75,7 +80,10 @@ namespace spot
is.boolean = false;
is.ltl_formula = false;
is.eltl_formula = false;
is.psl_formula = true;
is.sere_formula = false;
is.accepting_eword = false;
assert(child->is_sere_formula());
break;
}
}

10
src/ltltest/kind.test
View file

@ -1,5 +1,5 @@
#! /bin/sh
# Copyright (C) 2010 Laboratoire de Recherche et Developement to
# Copyright (C) 2010, 2011 Laboratoire de Recherche et Developement to
# l'Epita (LRDE).
#
# This file is part of Spot, a model checking library.
@ -33,10 +33,10 @@ check()
test "$word" = "$2"
}
check 'a' 'B&!xfLEP'
check 'a<->b' 'BxfLEP'
check '!a' 'B&!xfLEP'
check '!(a|b)' 'B&xfLEP'
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'