Add functions to compute the kind of a formula (LTL, PSL, Boolean...)
* src/ltlvisit/kind.hh, src/ltlvisit/kind.cc: New files. * src/ltlvisit/Makefile.am: Add them. * src/ltltest/kind.test, src/ltltest/kind.cc: New files. * src/ltltest/Makefile.am: Add them.
This commit is contained in:
Alexandre Duret-Lutz
parent
567b460738
commit
437128b55b
7 changed files with 434 additions and 0 deletions
2
src/ltltest/.gitignore
vendored
2
src/ltltest/.gitignore
vendored
|
|
@ -22,3 +22,5 @@ randltl
|
||||||
reductau
|
reductau
|
||||||
reductaustr
|
reductaustr
|
||||||
genltl
|
genltl
|
||||||
|
kind
|
||||||
|
consterm
|
||||||
|
|
|
||||||
|
|
@ -30,6 +30,7 @@ check_SCRIPTS = defs
|
||||||
check_PROGRAMS = \
|
check_PROGRAMS = \
|
||||||
consterm \
|
consterm \
|
||||||
equals \
|
equals \
|
||||||
|
kind \
|
||||||
length \
|
length \
|
||||||
ltl2dot \
|
ltl2dot \
|
||||||
ltl2text \
|
ltl2text \
|
||||||
|
|
@ -51,6 +52,7 @@ noinst_PROGRAMS = \
|
||||||
consterm_SOURCES = consterm.cc
|
consterm_SOURCES = consterm.cc
|
||||||
equals_SOURCES = equals.cc
|
equals_SOURCES = equals.cc
|
||||||
genltl_SOURCES = genltl.cc
|
genltl_SOURCES = genltl.cc
|
||||||
|
kind_SOURCES = kind.cc
|
||||||
length_SOURCES = length.cc
|
length_SOURCES = length.cc
|
||||||
ltl2dot_SOURCES = readltl.cc
|
ltl2dot_SOURCES = readltl.cc
|
||||||
ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY
|
ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY
|
||||||
|
|
@ -89,6 +91,7 @@ TESTS = \
|
||||||
nenoform.test \
|
nenoform.test \
|
||||||
tunenoform.test \
|
tunenoform.test \
|
||||||
consterm.test \
|
consterm.test \
|
||||||
|
kind.test \
|
||||||
syntimpl.test \
|
syntimpl.test \
|
||||||
reduc.test \
|
reduc.test \
|
||||||
reduccmp.test
|
reduccmp.test
|
||||||
|
|
|
||||||
57
src/ltltest/kind.cc
Normal file
57
src/ltltest/kind.cc
Normal file
|
|
@ -0,0 +1,57 @@
|
||||||
|
// Copyright (C) 2010 Laboratoire de Recherche et Developement de
|
||||||
|
// l'Epita (LRDE).
|
||||||
|
//
|
||||||
|
// This file is part of Spot, a model checking library.
|
||||||
|
//
|
||||||
|
// Spot is free software; you can redistribute it and/or modify it
|
||||||
|
// under the terms of the GNU General Public License as published by
|
||||||
|
// the Free Software Foundation; either version 2 of the License, or
|
||||||
|
// (at your option) any later version.
|
||||||
|
//
|
||||||
|
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||||
|
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||||
|
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||||
|
// License for more details.
|
||||||
|
//
|
||||||
|
// You should have received a copy of the GNU General Public License
|
||||||
|
// along with Spot; see the file COPYING. If not, write to the Free
|
||||||
|
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||||
|
// 02111-1307, USA.
|
||||||
|
|
||||||
|
#include <iostream>
|
||||||
|
#include <cassert>
|
||||||
|
#include <cstdlib>
|
||||||
|
#include "ltlparse/public.hh"
|
||||||
|
#include "ltlvisit/kind.hh"
|
||||||
|
#include "ltlast/allnodes.hh"
|
||||||
|
|
||||||
|
void
|
||||||
|
syntax(char *prog)
|
||||||
|
{
|
||||||
|
std::cerr << prog << " formula" << std::endl;
|
||||||
|
exit(2);
|
||||||
|
}
|
||||||
|
|
||||||
|
int
|
||||||
|
main(int argc, char **argv)
|
||||||
|
{
|
||||||
|
if (argc != 2)
|
||||||
|
syntax(argv[0]);
|
||||||
|
|
||||||
|
spot::ltl::parse_error_list p1;
|
||||||
|
spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
|
||||||
|
|
||||||
|
if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
|
||||||
|
return 2;
|
||||||
|
|
||||||
|
unsigned k = spot::ltl::kind_of(f1);
|
||||||
|
spot::ltl::print_kind(std::cout, k, true) << " = ";
|
||||||
|
spot::ltl::print_kind(std::cout, k, false) << std::endl;
|
||||||
|
|
||||||
|
f1->destroy();
|
||||||
|
assert(spot::ltl::atomic_prop::instance_count() == 0);
|
||||||
|
assert(spot::ltl::unop::instance_count() == 0);
|
||||||
|
assert(spot::ltl::binop::instance_count() == 0);
|
||||||
|
assert(spot::ltl::multop::instance_count() == 0);
|
||||||
|
return 0;
|
||||||
|
}
|
||||||
72
src/ltltest/kind.test
Executable file
72
src/ltltest/kind.test
Executable file
|
|
@ -0,0 +1,72 @@
|
||||||
|
#! /bin/sh
|
||||||
|
# Copyright (C) 2010 Laboratoire de Recherche et Developement to
|
||||||
|
# l'Epita (LRDE).
|
||||||
|
#
|
||||||
|
# This file is part of Spot, a model checking library.
|
||||||
|
#
|
||||||
|
# Spot is free software; you can redistribute it and/or modify it
|
||||||
|
# under the terms of the GNU General Public License as published by
|
||||||
|
# the Free Software Foundation; either version 2 of the License, or
|
||||||
|
# (at your option) any later version.
|
||||||
|
#
|
||||||
|
# Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||||
|
# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||||
|
# or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||||
|
# License for more details.
|
||||||
|
#
|
||||||
|
# You should have received a copy of the GNU General Public License
|
||||||
|
# along with Spot; see the file COPYING. If not, write to the Free
|
||||||
|
# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||||
|
# 02111-1307, USA.
|
||||||
|
|
||||||
|
|
||||||
|
# Check for the constant_term visitor
|
||||||
|
|
||||||
|
. ./defs || exit 1
|
||||||
|
|
||||||
|
set -e
|
||||||
|
|
||||||
|
check()
|
||||||
|
{
|
||||||
|
run 0 ../kind "$1" >out
|
||||||
|
read word rest <out
|
||||||
|
test "$word" = "$2"
|
||||||
|
}
|
||||||
|
|
||||||
|
check 'a' 'B&!xfLEP'
|
||||||
|
check 'a<->b' 'BxfLEP'
|
||||||
|
check '!a' 'B&!xfLEP'
|
||||||
|
check '!(a|b)' 'B&xfLEP'
|
||||||
|
check 'a U b' '&!xfLP'
|
||||||
|
check 'a U Fb' '&!xLP'
|
||||||
|
check 'Ga U b' '&!xLP'
|
||||||
|
check 'a W b' '&!xfLP'
|
||||||
|
check 'a M b' '&!xfLP'
|
||||||
|
check 'a R b' '&!xfLP'
|
||||||
|
check '{a}|->!Xb' '&fP'
|
||||||
|
check '{a}|->X!b' '&!fP'
|
||||||
|
check '{a}|->!Gb' '&xP'
|
||||||
|
check '{a}|->F!b' '&!xP'
|
||||||
|
|
||||||
|
run 0 ../consterm '1'
|
||||||
|
run 0 ../consterm '0'
|
||||||
|
run 1 ../consterm '[*0]'
|
||||||
|
run 1 ../consterm 'a*'
|
||||||
|
run 1 ../consterm '0*'
|
||||||
|
run 1 ../consterm 'a[*0]'
|
||||||
|
run 1 ../consterm 'a[*0..]'
|
||||||
|
run 1 ../consterm 'a[*0..3]'
|
||||||
|
run 0 ../consterm 'a[*1..3]'
|
||||||
|
run 0 ../consterm 'a[*3]'
|
||||||
|
run 1 ../consterm 'a[*..4][*3]'
|
||||||
|
run 0 ../consterm 'a[*1..4][*3]'
|
||||||
|
run 1 ../consterm 'a[*1..4][*0..3]'
|
||||||
|
run 0 ../consterm '((a ; b) + c)'
|
||||||
|
run 1 ../consterm '((a ; b) + [*0])'
|
||||||
|
run 0 ../consterm '((a ; b) + [*0]) & e'
|
||||||
|
run 1 ../consterm '((a ; b) + [*0]) & [*0]'
|
||||||
|
run 1 ../consterm '((a ; b) + [*0]) & (a* + b)'
|
||||||
|
run 1 ../consterm '{{a ; b} + {[*0]}} & {a* + b}' # test braces
|
||||||
|
run 1 ../consterm '(a + [*0]);(b + [*0]);(c + [*0])'
|
||||||
|
run 0 ../consterm '(a + [*0]);(b + e);(c + [*0])'
|
||||||
|
run 1 ../consterm '(a + [*0]);(b + e)*;(c + [*0])'
|
||||||
|
|
@ -35,6 +35,7 @@ ltlvisit_HEADERS = \
|
||||||
destroy.hh \
|
destroy.hh \
|
||||||
dotty.hh \
|
dotty.hh \
|
||||||
dump.hh \
|
dump.hh \
|
||||||
|
kind.hh \
|
||||||
length.hh \
|
length.hh \
|
||||||
lunabbrev.hh \
|
lunabbrev.hh \
|
||||||
mark.hh \
|
mark.hh \
|
||||||
|
|
@ -57,6 +58,7 @@ libltlvisit_la_SOURCES = \
|
||||||
destroy.cc \
|
destroy.cc \
|
||||||
dotty.cc \
|
dotty.cc \
|
||||||
dump.cc \
|
dump.cc \
|
||||||
|
kind.cc \
|
||||||
length.cc \
|
length.cc \
|
||||||
lunabbrev.cc \
|
lunabbrev.cc \
|
||||||
mark.cc \
|
mark.cc \
|
||||||
|
|
|
||||||
229
src/ltlvisit/kind.cc
Normal file
229
src/ltlvisit/kind.cc
Normal file
|
|
@ -0,0 +1,229 @@
|
||||||
|
// Copyright (C) 2010 Laboratoire de Recherche et Développement
|
||||||
|
// de l'Epita (LRDE).
|
||||||
|
//
|
||||||
|
// This file is part of Spot, a model checking library.
|
||||||
|
//
|
||||||
|
// Spot is free software; you can redistribute it and/or modify it
|
||||||
|
// under the terms of the GNU General Public License as published by
|
||||||
|
// the Free Software Foundation; either version 2 of the License, or
|
||||||
|
// (at your option) any later version.
|
||||||
|
//
|
||||||
|
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||||
|
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||||
|
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||||
|
// License for more details.
|
||||||
|
//
|
||||||
|
// You should have received a copy of the GNU General Public License
|
||||||
|
// along with Spot; see the file COPYING. If not, write to the Free
|
||||||
|
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||||
|
// 02111-1307, USA.
|
||||||
|
|
||||||
|
#include "kind.hh"
|
||||||
|
#include "ltlast/allnodes.hh"
|
||||||
|
#include "ltlast/visitor.hh"
|
||||||
|
#include <iostream>
|
||||||
|
|
||||||
|
namespace spot
|
||||||
|
{
|
||||||
|
namespace ltl
|
||||||
|
{
|
||||||
|
namespace
|
||||||
|
{
|
||||||
|
|
||||||
|
class kind_visitor : public visitor
|
||||||
|
{
|
||||||
|
unsigned result_;
|
||||||
|
public:
|
||||||
|
kind_visitor()
|
||||||
|
: result_(All_Kind)
|
||||||
|
{
|
||||||
|
}
|
||||||
|
~kind_visitor()
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
|
unsigned
|
||||||
|
result()
|
||||||
|
{
|
||||||
|
return result_;
|
||||||
|
}
|
||||||
|
|
||||||
|
void
|
||||||
|
visit(atomic_prop*)
|
||||||
|
{
|
||||||
|
}
|
||||||
|
|
||||||
|
void
|
||||||
|
visit(constant* c)
|
||||||
|
{
|
||||||
|
if (c == constant::empty_word_instance())
|
||||||
|
result_ &= ~(Boolean_Kind | LTL_Kind | ELTL_Kind);
|
||||||
|
}
|
||||||
|
|
||||||
|
void
|
||||||
|
visit(bunop* bo)
|
||||||
|
{
|
||||||
|
result_ = recurse(bo->child());
|
||||||
|
result_ &= ~(Boolean_Kind | LTL_Kind | ELTL_Kind);
|
||||||
|
}
|
||||||
|
|
||||||
|
void
|
||||||
|
visit(unop* uo)
|
||||||
|
{
|
||||||
|
result_ = recurse(uo->child());
|
||||||
|
|
||||||
|
switch (uo->op())
|
||||||
|
{
|
||||||
|
case unop::NegClosure:
|
||||||
|
case unop::Closure:
|
||||||
|
result_ &= ~(Boolean_Kind | LTL_Kind | ELTL_Kind);
|
||||||
|
return;
|
||||||
|
case unop::Finish:
|
||||||
|
result_ &= ~(Boolean_Kind | LTL_Kind | PSL_Kind);
|
||||||
|
return;
|
||||||
|
case unop::Not:
|
||||||
|
if (!dynamic_cast<atomic_prop*>(uo->child()))
|
||||||
|
result_ &= ~NeNoForm_Kind;
|
||||||
|
return;
|
||||||
|
case unop::X:
|
||||||
|
result_ &= ~(Boolean_Kind | No_X_Kind | ELTL_Kind);
|
||||||
|
return;
|
||||||
|
case unop::F:
|
||||||
|
case unop::G:
|
||||||
|
result_ &= ~(Boolean_Kind | SugarFree_LTL_Kind | ELTL_Kind);
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
/* Unreachable code. */
|
||||||
|
assert(0);
|
||||||
|
}
|
||||||
|
|
||||||
|
void
|
||||||
|
visit(automatop* ao)
|
||||||
|
{
|
||||||
|
unsigned aos = ao->size();
|
||||||
|
for (unsigned i = 0; i < aos && !result_; ++i)
|
||||||
|
result_ &= recurse(ao->nth(i));
|
||||||
|
|
||||||
|
result_ &= ~(Boolean_Kind | LTL_Kind | PSL_Kind);
|
||||||
|
}
|
||||||
|
|
||||||
|
void
|
||||||
|
visit(multop* mo)
|
||||||
|
{
|
||||||
|
unsigned mos = mo->size();
|
||||||
|
for (unsigned i = 0; i < mos && !result_; ++i)
|
||||||
|
result_ &= recurse(mo->nth(i));
|
||||||
|
|
||||||
|
switch (mo->op())
|
||||||
|
{
|
||||||
|
case multop::Or:
|
||||||
|
case multop::And:
|
||||||
|
return;
|
||||||
|
case multop::AndNLM:
|
||||||
|
// The non-matching-length-And (&) can only appear
|
||||||
|
// in the rational parts of PSL formula. We
|
||||||
|
// don't remove the Boolean_Kind flags, because
|
||||||
|
// applied to atomic propositions a&b has the same
|
||||||
|
// effect as a&&b.
|
||||||
|
result_ &= ~(LTL_Kind | ELTL_Kind);
|
||||||
|
return;
|
||||||
|
case multop::Concat:
|
||||||
|
case multop::Fusion:
|
||||||
|
result_ &= ~(Boolean_Kind | LTL_Kind | ELTL_Kind);
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
void
|
||||||
|
visit(binop* bo)
|
||||||
|
{
|
||||||
|
result_ = recurse(bo->first()) & recurse(bo->second());
|
||||||
|
|
||||||
|
switch (bo->op())
|
||||||
|
{
|
||||||
|
case binop::EConcatMarked:
|
||||||
|
case binop::UConcat:
|
||||||
|
case binop::EConcat:
|
||||||
|
result_ &= ~(Boolean_Kind | LTL_Kind | ELTL_Kind);
|
||||||
|
return;
|
||||||
|
case binop::Xor:
|
||||||
|
case binop::Implies:
|
||||||
|
case binop::Equiv:
|
||||||
|
result_ &= ~(NeNoForm_Kind | SugarFree_Boolean_Kind);
|
||||||
|
return;
|
||||||
|
case binop::U:
|
||||||
|
case binop::W:
|
||||||
|
case binop::M:
|
||||||
|
case binop::R:
|
||||||
|
result_ &= ~(Boolean_Kind | ELTL_Kind);
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
/* Unreachable code. */
|
||||||
|
assert(0);
|
||||||
|
}
|
||||||
|
|
||||||
|
unsigned
|
||||||
|
recurse(const formula* f)
|
||||||
|
{
|
||||||
|
return kind_of(f);
|
||||||
|
}
|
||||||
|
};
|
||||||
|
}
|
||||||
|
|
||||||
|
unsigned
|
||||||
|
kind_of(const formula* f)
|
||||||
|
{
|
||||||
|
kind_visitor v;
|
||||||
|
const_cast<formula*>(f)->accept(v);
|
||||||
|
return v.result();
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
std::ostream&
|
||||||
|
print_kind(std::ostream& o, unsigned k, bool abbreviated)
|
||||||
|
{
|
||||||
|
struct data { char abbrev; const char* name; };
|
||||||
|
static const data kind_name[] =
|
||||||
|
{
|
||||||
|
{'B', "Boolean formula"}, // 1
|
||||||
|
{'&', "no sugar Boolean operator"}, // 2
|
||||||
|
{'!', "in negative normal form"}, // 4
|
||||||
|
{'x', "no X LTL operator"}, // 8
|
||||||
|
{'f', "no sugar LTL operator"}, // 16
|
||||||
|
{'L', "LTL formula"}, // 32
|
||||||
|
{'E', "ELTL formula"}, // 64
|
||||||
|
{'P', "PSL formula"}, // 128
|
||||||
|
};
|
||||||
|
const char* comma = "";
|
||||||
|
unsigned size = (sizeof kind_name)/(sizeof *kind_name);
|
||||||
|
for (unsigned i = 0; i < size; ++i)
|
||||||
|
{
|
||||||
|
if ((k & 1))
|
||||||
|
{
|
||||||
|
if (abbreviated)
|
||||||
|
{
|
||||||
|
o << kind_name[i].abbrev;
|
||||||
|
}
|
||||||
|
else
|
||||||
|
{
|
||||||
|
o << comma << kind_name[i].name;
|
||||||
|
comma = ", ";
|
||||||
|
}
|
||||||
|
}
|
||||||
|
k >>= 1;
|
||||||
|
}
|
||||||
|
return o;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
std::ostream&
|
||||||
|
print_kind(std::ostream& o, const formula* f, bool abbreviated)
|
||||||
|
{
|
||||||
|
print_kind(o, kind_of(f), abbreviated);
|
||||||
|
return o;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
}
|
||||||
|
}
|
||||||
69
src/ltlvisit/kind.hh
Normal file
69
src/ltlvisit/kind.hh
Normal file
|
|
@ -0,0 +1,69 @@
|
||||||
|
// Copyright (C) 2010 Laboratoire de Recherche et Développement de
|
||||||
|
// l'Epita (LRDE).
|
||||||
|
//
|
||||||
|
// This file is part of Spot, a model checking library.
|
||||||
|
//
|
||||||
|
// Spot is free software; you can redistribute it and/or modify it
|
||||||
|
// under the terms of the GNU General Public License as published by
|
||||||
|
// the Free Software Foundation; either version 2 of the License, or
|
||||||
|
// (at your option) any later version.
|
||||||
|
//
|
||||||
|
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||||
|
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||||
|
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||||
|
// License for more details.
|
||||||
|
//
|
||||||
|
// You should have received a copy of the GNU General Public License
|
||||||
|
// along with Spot; see the file COPYING. If not, write to the Free
|
||||||
|
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||||
|
// 02111-1307, USA.
|
||||||
|
|
||||||
|
#ifndef SPOT_LTLVISIT_KIND_HH
|
||||||
|
# define SPOT_LTLVISIT_KIND_HH
|
||||||
|
|
||||||
|
#include "ltlast/predecl.hh"
|
||||||
|
#include <iosfwd>
|
||||||
|
|
||||||
|
namespace spot
|
||||||
|
{
|
||||||
|
namespace ltl
|
||||||
|
{
|
||||||
|
/// Different kinds or proporties of formulae.
|
||||||
|
// If you change this list, you have to adjust
|
||||||
|
// the kind_name array in print_kind() (kind.cc)
|
||||||
|
enum kind
|
||||||
|
{
|
||||||
|
Boolean_Kind = 1,
|
||||||
|
SugarFree_Boolean_Kind = 2,
|
||||||
|
NeNoForm_Kind = 4,
|
||||||
|
No_X_Kind = 8,
|
||||||
|
SugarFree_LTL_Kind = 16,
|
||||||
|
LTL_Kind = 32,
|
||||||
|
ELTL_Kind = 64,
|
||||||
|
PSL_Kind = 128,
|
||||||
|
All_Kind = -1U,
|
||||||
|
};
|
||||||
|
|
||||||
|
|
||||||
|
/// \brief Compute properties of a formula.
|
||||||
|
/// \ingroup ltl_visitor
|
||||||
|
///
|
||||||
|
/// Return a sum of ltl::kind values depending on the operators
|
||||||
|
/// used by a formula.
|
||||||
|
///
|
||||||
|
/// \param f The formula to analyze.
|
||||||
|
unsigned kind_of(const formula* f);
|
||||||
|
|
||||||
|
/// \brief Print a ltl::kind (computed by kind_of()).
|
||||||
|
/// \ingroup ltl_visitor
|
||||||
|
std::ostream& print_kind(std::ostream& o, unsigned k,
|
||||||
|
bool abbreviated = false);
|
||||||
|
|
||||||
|
/// \brief Print the properties of a formula.
|
||||||
|
/// \ingroup ltl_visitor
|
||||||
|
std::ostream& print_kind(std::ostream& o, const formula* f,
|
||||||
|
bool abbreviated = false);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
#endif // SPOT_LTLVISIT_KIND_HH
|
||||||
Loading…
Add table
Add a link
Reference in a new issue