* src/sanity/80columns.test: New file.
* src/sanity/Makefile.am (check-local): Run it. * src/ltltest/equals.test, src/ltltest/lunabbrev.test, src/ltltest/nenoform.test, src/ltltest/parseerr.test src/ltltest/tunabbrev.test, src/ltlvisit/forminf.cc, src/tgbatest/explpro2.test, src/tgbatest/explpro3.test, src/tgbatest/explprod.test, src/tgbatest/spotlbtt.test, src/tgbatest/tripprod.test: Wrap long lines.
This commit is contained in:
Alexandre Duret-Lutz
parent
e69d0fa94e
commit
83de4264cb
15 changed files with 180 additions and 115 deletions
12
ChangeLog
12
ChangeLog
|
|
@ -1,3 +1,15 @@
|
|||
2004-05-10 Alexandre Duret-Lutz <adl@src.lip6.fr>
|
||||
|
||||
* src/sanity/80columns.test: New file.
|
||||
* src/sanity/Makefile.am (check-local): Run it.
|
||||
* src/ltltest/equals.test, src/ltltest/lunabbrev.test,
|
||||
src/ltltest/nenoform.test, src/ltltest/parseerr.test
|
||||
src/ltltest/tunabbrev.test, src/ltltest/reduc.cc,
|
||||
src/ltltest/tunabbrev.test, src/ltlvisit/forminf.cc,
|
||||
src/tgbatest/explpro2.test, src/tgbatest/explpro3.test,
|
||||
src/tgbatest/explprod.test, src/tgbatest/spotlbtt.test,
|
||||
src/tgbatest/tripprod.test: Wrap long lines.
|
||||
|
||||
2004-05-10 Thomas MARTINEZ <martinez@abacus.lip6.fr>
|
||||
|
||||
* src/tgbatest/ltl2tgba.cc (main): Add a option for reduce the formula.
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#! /bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -39,7 +39,8 @@ run 0 ./equals 'a & b & c' 'b & c & a'
|
|||
run 0 ./equals 'a && b & a' 'b & a & b'
|
||||
run 0 ./equals 'a & b' 'b & a & b'
|
||||
run 0 ./equals 'a & b' 'b & a & a'
|
||||
run 0 ./equals 'a & b & (c |(f U g)|| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
|
||||
run 0 ./equals 'a & b & (c |(f U g)|| e)' \
|
||||
'b & a & a & (c | e |(f U g)| e | c) & b'
|
||||
run 0 ./equals 'a & a' 'a'
|
||||
|
||||
# other formulae which are not
|
||||
|
|
@ -51,7 +52,8 @@ run 1 ./equals 'a => b' 'a U b'
|
|||
run 1 ./equals 'a R b' 'a U b'
|
||||
run 1 ./equals 'a & b & c' 'c & a'
|
||||
run 1 ./equals 'b & c' 'c & a & b'
|
||||
run 1 ./equals 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(g U g)| e | c) & b'
|
||||
run 1 ./equals 'a & b & (c |(f U g)| e)' \
|
||||
'b & a & a & (c | e |(g U g)| e | c) & b'
|
||||
|
||||
# Precedence
|
||||
run 0 ./equals 'a & b ^ c | d' 'd | c ^ b & a'
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#! /bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -40,10 +40,12 @@ run 0 ./lunabbrev 'a & b & c' 'b & c & a'
|
|||
run 0 ./lunabbrev 'a & b & a' 'b & a & b'
|
||||
run 0 ./lunabbrev 'a & b' 'b & a & b'
|
||||
run 0 ./lunabbrev 'a & b' 'b & a & a'
|
||||
run 0 ./lunabbrev 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
|
||||
run 0 ./lunabbrev 'a & b & (c |(f U g)| e)' \
|
||||
'b & a & a & (c | e |(f U g)| e | c) & b'
|
||||
# other formulae that do change
|
||||
run 0 ./lunabbrev 'a ^ b' '(a & !b) | (!a & b)'
|
||||
run 0 ./lunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
|
||||
run 0 ./lunabbrev 'GF a => F G(b)' '!GFa | F Gb'
|
||||
run 0 ./lunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
|
||||
run 0 ./lunabbrev '(a ^ b) | (b ^ c)' '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
|
||||
run 0 ./lunabbrev '(a ^ b) | (b ^ c)' \
|
||||
'(c & !b) | (!c & b) | (a & !b) | (!a & b)'
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#! /bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -40,7 +40,8 @@ run 0 ./nenoform 'a & b & c' 'b & c & a'
|
|||
run 0 ./nenoform 'Xa & b & Xa' 'b & Xa & b'
|
||||
run 0 ./nenoform 'a & b' 'b & a & b'
|
||||
run 0 ./nenoform 'a & !b' '!b & a & a'
|
||||
run 0 ./nenoform 'a & b & (Xc |(f U !g)| e)' 'b & a & a & (Xc | e |(f U !g)| e | Xc) & b'
|
||||
run 0 ./nenoform 'a & b & (Xc |(f U !g)| e)' \
|
||||
'b & a & a & (Xc | e |(f U !g)| e | Xc) & b'
|
||||
run 0 ./nenoform 'GFa => FGb' 'GFa => FGb'
|
||||
|
||||
# Basic rewritings
|
||||
|
|
@ -60,5 +61,6 @@ run 0 ./nenoform '!(a & b & c & d & b)' '!a | !b | !c | !d'
|
|||
run 0 ./nenoform '!(a | b | c | d)' '!a & !b & !c & !d'
|
||||
|
||||
# Nested rewritings
|
||||
run 0 ./nenoform '!(a U (!b U ((a & b & c) R d)))' '!a R (b R ((!a | !b | !c) U !d))'
|
||||
run 0 ./nenoform '!(a U (!b U ((a & b & c) R d)))' \
|
||||
'!a R (b R ((!a | !b | !c) U !d))'
|
||||
run 0 ./nenoform '!(GF a => FG b)' 'GFa & GF!b'
|
||||
|
|
|
|||
|
|
@ -56,7 +56,8 @@ check 'a U b c' 'binop(U, AP(a), AP(b))'
|
|||
check 'a &&& b' 'multop(And, constant(0), AP(b))'
|
||||
# (check multop merging while we are at it)
|
||||
check 'a & b & c & d e' 'multop(And, AP(a), AP(b), AP(c), AP(d))'
|
||||
check 'a & (b | c) & d should work' 'multop(And, AP(a), multop(Or, AP(b), AP(c)), AP(d))'
|
||||
check 'a & (b | c) & d should work' \
|
||||
'multop(And, AP(a), multop(Or, AP(b), AP(c)), AP(d))'
|
||||
|
||||
# Binop recovery
|
||||
check 'a U' 'constant(0)'
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
|
|
@ -45,7 +45,7 @@ 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);
|
||||
spot::ltl::formula* f2 = NULL;
|
||||
|
|
@ -53,37 +53,37 @@ main(int argc, char** argv)
|
|||
if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
|
||||
return 2;
|
||||
|
||||
|
||||
|
||||
if (argc == 3){
|
||||
spot::ltl::parse_error_list p2;
|
||||
f2 = spot::ltl::parse(argv[2], p2);
|
||||
if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2))
|
||||
return 2;
|
||||
}
|
||||
|
||||
|
||||
int exit_code = 0;
|
||||
|
||||
|
||||
spot::ltl::formula* ftmp1;
|
||||
spot::ltl::formula* ftmp2;
|
||||
|
||||
|
||||
ftmp1 = f1;
|
||||
f1 = unabbreviate_logic(f1);
|
||||
ftmp2 = f1;
|
||||
f1 = negative_normal_form(f1);
|
||||
spot::ltl::destroy(ftmp1);
|
||||
spot::ltl::destroy(ftmp2);
|
||||
|
||||
|
||||
|
||||
|
||||
int length_f1_before = spot::ltl::form_length(f1);
|
||||
std::string f1s_before = spot::ltl::to_string(f1);
|
||||
|
||||
|
||||
ftmp1 = f1;
|
||||
f1 = spot::ltl::reduce(f1);
|
||||
ftmp2 = f1;
|
||||
f1 = spot::ltl::unabbreviate_logic(f1);
|
||||
spot::ltl::destroy(ftmp1);
|
||||
spot::ltl::destroy(ftmp2);
|
||||
|
||||
|
||||
int length_f1_after = spot::ltl::form_length(f1);
|
||||
std::string f1s_after = spot::ltl::to_string(f1);
|
||||
|
||||
|
|
@ -102,49 +102,54 @@ main(int argc, char** argv)
|
|||
spot::ltl::destroy(ftmp1);
|
||||
f2s = spot::ltl::to_string(f2);
|
||||
}
|
||||
|
||||
|
||||
|
||||
|
||||
if (red && (f2 == NULL)) {
|
||||
std::cout << length_f1_before << " " << length_f1_after
|
||||
<< " '" << f1s_before << "' reduce to '" << f1s_after << "'" << std::endl;
|
||||
std::cout << length_f1_before << " " << length_f1_after
|
||||
<< " '" << f1s_before << "' reduce to '" << f1s_after << "'"
|
||||
<< std::endl;
|
||||
}
|
||||
|
||||
|
||||
if (f2 != NULL){
|
||||
if (f1 != f2) {
|
||||
if (length_f1_after < length_f1_before)
|
||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after << " KOREDUC " << std::endl;
|
||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
|
||||
<< " KOREDUC " << std::endl;
|
||||
else
|
||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after << " KOIDEM " << std::endl;
|
||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
|
||||
<< " KOIDEM " << std::endl;
|
||||
exit_code = 1;
|
||||
}
|
||||
else {
|
||||
if (f1s_before != f1s_after)
|
||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after << " OKREDUC " << std::endl;
|
||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
|
||||
<< " OKREDUC " << std::endl;
|
||||
else
|
||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after << " OKIDEM" << std::endl;
|
||||
std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after
|
||||
<< " OKIDEM" << std::endl;
|
||||
exit_code = 0;
|
||||
}
|
||||
}
|
||||
else{
|
||||
else{
|
||||
if (length_f1_after < length_f1_before) exit_code = 0;
|
||||
}
|
||||
|
||||
|
||||
/*
|
||||
spot::ltl::dump(std::cout, f1); std::cout << std::endl;
|
||||
if (f2 != NULL)
|
||||
spot::ltl::dump(std::cout, f2); std::cout << std::endl;
|
||||
*/
|
||||
|
||||
|
||||
|
||||
|
||||
spot::ltl::destroy(f1);
|
||||
if (f2 != NULL)
|
||||
spot::ltl::destroy(f2);
|
||||
|
||||
|
||||
|
||||
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 exit_code;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#! /bin/sh
|
||||
# Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
# département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
# et Marie Curie.
|
||||
#
|
||||
|
|
@ -39,16 +39,19 @@ run 0 ./tunabbrev 'a & b & c' 'b & c & a'
|
|||
run 0 ./tunabbrev 'a & b & a' 'b & a & b'
|
||||
run 0 ./tunabbrev 'a & b' 'b & a & b'
|
||||
run 0 ./tunabbrev 'a & b' 'b & a & a'
|
||||
run 0 ./tunabbrev 'a & b & (c |(f U g)| e)' 'b & a & a & (c | e |(f U g)| e | c) & b'
|
||||
run 0 ./tunabbrev 'a & b & (c |(f U g)| e)' \
|
||||
'b & a & a & (c | e |(f U g)| e | c) & b'
|
||||
|
||||
# same as in lunabbrev.test:
|
||||
run 0 ./tunabbrev 'a ^ b' '(a & !b) | (!a & b)'
|
||||
run 0 ./tunabbrev 'a ^ Xb' '(!Xb & a) | (!a & Xb) | (Xb & !a)'
|
||||
run 0 ./tunabbrev '!a <-> Xb' '(Xb & !a) | (!!a & !Xb)'
|
||||
run 0 ./tunabbrev '(a ^ b) | (b ^ c)' '(c & !b) | (!c & b) | (a & !b) | (!a & b)'
|
||||
run 0 ./tunabbrev '(a ^ b) | (b ^ c)' \
|
||||
'(c & !b) | (!c & b) | (a & !b) | (!a & b)'
|
||||
|
||||
# LTL unabbreviations:
|
||||
run 0 ./tunabbrev 'G a ' 'false R a'
|
||||
run 0 ./tunabbrev 'GF a => F G(b)' '!(false R (true U a)) | (true U (false V b))'
|
||||
run 0 ./tunabbrev 'GF a => F G(b)' \
|
||||
'!(false R (true U a)) | (true U (false V b))'
|
||||
run 0 ./tunabbrev 'GGGGa' 'false V (false V (false V (false V a)))'
|
||||
run 0 ./tunabbrev 'FFFfalse' 'true U ((true) U (true U (false)))'
|
||||
|
|
|
|||
|
|
@ -1,4 +1,4 @@
|
|||
// Copyright (C) 2003 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
|
|
@ -42,7 +42,7 @@ namespace spot
|
|||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
bool
|
||||
is_FG(const formula* f)
|
||||
{
|
||||
|
|
@ -58,47 +58,47 @@ namespace spot
|
|||
nb_term_multop(const formula* f)
|
||||
{
|
||||
if ((const multop*)f == NULL) return -1;
|
||||
|
||||
|
||||
unsigned mos = ((const multop*)(f))->size();
|
||||
return mos;
|
||||
}
|
||||
|
||||
|
||||
|
||||
node_type_form_visitor::node_type_form_visitor(){}
|
||||
|
||||
|
||||
node_type_form_visitor::type
|
||||
node_type_form_visitor::result() const { return result_;}
|
||||
|
||||
|
||||
void
|
||||
node_type_form_visitor::visit(const atomic_prop* ap){
|
||||
node_type_form_visitor::visit(const atomic_prop* ap){
|
||||
if (ap == NULL);
|
||||
result_ = node_type_form_visitor::Atom;
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
node_type_form_visitor::visit(const constant* c){
|
||||
node_type_form_visitor::visit(const constant* c){
|
||||
if (c == NULL);
|
||||
result_ = node_type_form_visitor::Const;
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
node_type_form_visitor::visit(const unop* uo){
|
||||
if (uo == NULL);
|
||||
if (uo == NULL);
|
||||
result_ = node_type_form_visitor::Unop;
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
node_type_form_visitor::visit(const binop* bo){
|
||||
node_type_form_visitor::visit(const binop* bo){
|
||||
if (bo == NULL);
|
||||
result_ = node_type_form_visitor::Binop;
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
node_type_form_visitor::visit(const multop* mo){
|
||||
node_type_form_visitor::visit(const multop* mo){
|
||||
if (mo == NULL);
|
||||
result_ = node_type_form_visitor::Multop;
|
||||
}
|
||||
|
||||
|
||||
node_type_form_visitor::type node_type(const formula* f)
|
||||
{
|
||||
node_type_form_visitor v;
|
||||
|
|
@ -110,41 +110,41 @@ namespace spot
|
|||
class form_eventual_universal_visitor : public const_visitor
|
||||
{
|
||||
public:
|
||||
|
||||
|
||||
form_eventual_universal_visitor()
|
||||
{
|
||||
eventual = false; // faux au départ
|
||||
universal = false;
|
||||
}
|
||||
|
||||
|
||||
virtual ~form_eventual_universal_visitor()
|
||||
{
|
||||
}
|
||||
|
||||
bool
|
||||
bool
|
||||
is_eventual() const
|
||||
{
|
||||
return eventual;
|
||||
}
|
||||
|
||||
bool
|
||||
|
||||
bool
|
||||
is_universal() const
|
||||
{
|
||||
return universal;
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
visit(const atomic_prop* ap)
|
||||
{
|
||||
if (ap);
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
visit(const constant* c)
|
||||
{
|
||||
if (c->val());
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
visit(const unop* uo)
|
||||
{
|
||||
|
|
@ -156,7 +156,7 @@ namespace spot
|
|||
eventual = recurse_ev(f1);
|
||||
universal = recurse_un(f1);
|
||||
return;
|
||||
case unop::F:
|
||||
case unop::F:
|
||||
eventual = true;
|
||||
return;
|
||||
case unop::G:
|
||||
|
|
@ -166,7 +166,7 @@ namespace spot
|
|||
/* Unreachable code. */
|
||||
assert(0);
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
visit(const binop* bo)
|
||||
{
|
||||
|
|
@ -191,13 +191,13 @@ namespace spot
|
|||
/* Unreachable code. */
|
||||
assert(0);
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
visit(const multop* mo)
|
||||
{
|
||||
if (mo == NULL);
|
||||
unsigned mos = mo->size();
|
||||
|
||||
|
||||
eventual = true;
|
||||
universal = true;
|
||||
for (unsigned i = 0; i < mos; ++i){
|
||||
|
|
@ -213,7 +213,7 @@ namespace spot
|
|||
}
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
bool
|
||||
recurse_ev(const formula* f)
|
||||
{
|
||||
|
|
@ -235,7 +235,7 @@ namespace spot
|
|||
bool universal;
|
||||
};
|
||||
|
||||
|
||||
|
||||
bool is_eventual(const formula* f)
|
||||
{
|
||||
form_eventual_universal_visitor v;
|
||||
|
|
@ -249,19 +249,19 @@ namespace spot
|
|||
const_cast<formula*>(f)->accept(v);
|
||||
return v.is_universal();
|
||||
}
|
||||
|
||||
|
||||
/////////////////////////////////////////////////////////////////////////
|
||||
|
||||
class inf_form_right_recurse_visitor : public const_visitor
|
||||
{
|
||||
public:
|
||||
|
||||
|
||||
inf_form_right_recurse_visitor(const formula *f)
|
||||
{
|
||||
this->f = f;
|
||||
result_ = false; // faux au départ
|
||||
}
|
||||
|
||||
|
||||
virtual ~inf_form_right_recurse_visitor()
|
||||
{
|
||||
}
|
||||
|
|
@ -278,19 +278,19 @@ namespace spot
|
|||
return false;
|
||||
}
|
||||
*/
|
||||
int
|
||||
int
|
||||
result() const
|
||||
{
|
||||
return result_;
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
visit(const atomic_prop* ap)
|
||||
{
|
||||
if ((const atomic_prop*)f == ap)
|
||||
if ((const atomic_prop*)f == ap)
|
||||
result_ = true;
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
visit(const constant* c)
|
||||
{
|
||||
|
|
@ -304,7 +304,7 @@ namespace spot
|
|||
return;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
visit(const unop* uo)
|
||||
{
|
||||
|
|
@ -316,7 +316,7 @@ namespace spot
|
|||
return;
|
||||
case unop::X:// à gérer !!
|
||||
return;
|
||||
case unop::F:
|
||||
case unop::F:
|
||||
// F(a) = true U a
|
||||
result_ = inf_form(f,f1);
|
||||
return;
|
||||
|
|
@ -331,7 +331,7 @@ namespace spot
|
|||
/* Unreachable code. */
|
||||
assert(0);
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
visit(const binop* bo)
|
||||
{
|
||||
|
|
@ -355,7 +355,7 @@ namespace spot
|
|||
/* Unreachable code. */
|
||||
assert(0);
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
visit(const multop* mo)
|
||||
{
|
||||
|
|
@ -377,7 +377,7 @@ namespace spot
|
|||
break;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
bool
|
||||
recurse(const formula* f1, const formula* f2)
|
||||
{
|
||||
|
|
@ -397,34 +397,35 @@ namespace spot
|
|||
class inf_form_left_recurse_visitor : public const_visitor
|
||||
{
|
||||
public:
|
||||
|
||||
|
||||
inf_form_left_recurse_visitor(const formula *f)
|
||||
{
|
||||
this->f = f;
|
||||
result_ = false;
|
||||
}
|
||||
|
||||
|
||||
virtual ~inf_form_left_recurse_visitor()
|
||||
{
|
||||
}
|
||||
|
||||
bool special_case(const formula* f2)
|
||||
{
|
||||
if ((node_type(f) == node_type_form_visitor::Binop)
|
||||
if ((node_type(f) == node_type_form_visitor::Binop)
|
||||
&& (node_type(f2) == node_type_form_visitor::Binop))
|
||||
if (((const binop*)f)->op() == ((const binop*)f2)->op())
|
||||
if (inf_form(((const binop*)f2)->first(),((const binop*)f)->first())
|
||||
&& inf_form(((const binop*)f2)->second(),((const binop*)f)->second()) )
|
||||
&& inf_form(((const binop*)f2)->second(),
|
||||
((const binop*)f)->second()))
|
||||
return true;
|
||||
return false;
|
||||
}
|
||||
|
||||
int
|
||||
int
|
||||
result() const
|
||||
{
|
||||
return result_;
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
visit(const atomic_prop* ap)
|
||||
{
|
||||
|
|
@ -432,7 +433,7 @@ namespace spot
|
|||
const_cast<formula*>(f)->accept(v);
|
||||
result_ = v.result();
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
visit(const constant* c)
|
||||
{
|
||||
|
|
@ -450,7 +451,7 @@ namespace spot
|
|||
/* Unreachable code. */
|
||||
assert(0);
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
visit(const unop* uo)
|
||||
{
|
||||
|
|
@ -469,7 +470,7 @@ namespace spot
|
|||
result_ = inf_form(f1,((const unop*)f)->child());
|
||||
}
|
||||
return;
|
||||
case unop::F:
|
||||
case unop::F:
|
||||
// F(a) = true U a
|
||||
tmp = binop::instance(binop::U,constant::true_instance(),clone(f1));
|
||||
if (this->special_case(tmp)){
|
||||
|
|
@ -483,7 +484,8 @@ namespace spot
|
|||
return;
|
||||
case unop::G:
|
||||
// F(a) = false R a
|
||||
tmp = binop::instance(binop::R,constant::false_instance(),clone(f1));
|
||||
tmp = binop::instance(binop::R,
|
||||
constant::false_instance(), clone(f1));
|
||||
if (this->special_case(tmp)){
|
||||
result_ = true;
|
||||
spot::ltl::destroy(tmp);
|
||||
|
|
@ -497,17 +499,17 @@ namespace spot
|
|||
/* Unreachable code. */
|
||||
assert(0);
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
visit(const binop* bo)
|
||||
{
|
||||
|
||||
|
||||
if (this->special_case(bo))
|
||||
{
|
||||
result_ = true;
|
||||
return;
|
||||
}
|
||||
|
||||
|
||||
const formula* f1 = bo->first();
|
||||
const formula* f2 = bo->second();
|
||||
switch (bo->op())
|
||||
|
|
@ -520,7 +522,7 @@ namespace spot
|
|||
if ( (inf_form(f1,f)) && (inf_form(f2,f)) )
|
||||
result_ = true;
|
||||
return;
|
||||
case binop::R:
|
||||
case binop::R:
|
||||
if ( (inf_form(f2,f)) )
|
||||
result_ = true;
|
||||
return;
|
||||
|
|
@ -528,7 +530,7 @@ namespace spot
|
|||
/* Unreachable code. */
|
||||
assert(0);
|
||||
}
|
||||
|
||||
|
||||
void
|
||||
visit(const multop* mo)
|
||||
{
|
||||
|
|
@ -550,7 +552,7 @@ namespace spot
|
|||
break;
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
protected:
|
||||
bool result_; // true if f1 < f, 1 otherwise.
|
||||
const formula* f;
|
||||
|
|
@ -558,19 +560,19 @@ namespace spot
|
|||
|
||||
bool inf_form(const formula* f1, const formula* f2)
|
||||
{
|
||||
// f1 and f2 are unabbreviate
|
||||
// f1 and f2 are unabbreviate
|
||||
if (f1 == f2) return true;
|
||||
inf_form_left_recurse_visitor v1(f2);
|
||||
inf_form_right_recurse_visitor v2(f1);
|
||||
|
||||
if ( (node_type(f1) == node_type_form_visitor::Const) &&
|
||||
|
||||
if ( (node_type(f1) == node_type_form_visitor::Const) &&
|
||||
(node_type(f2) == node_type_form_visitor::Const) )
|
||||
if ( (((const constant*)f2)->val() == constant::True) ||
|
||||
(((const constant*)f1)->val() == constant::False) )
|
||||
{
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
const_cast<formula*>(f1)->accept(v1);
|
||||
if (v1.result()) {
|
||||
return true;
|
||||
|
|
@ -580,38 +582,39 @@ namespace spot
|
|||
if (v2.result()) {
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
|
||||
bool infneg_form(const formula* f1, const formula* f2, int n)
|
||||
{
|
||||
const formula* ftmp1;
|
||||
const formula* ftmp2;
|
||||
const formula* ftmp3 = unop::instance(unop::Not,(n == 0)? clone(f1) : clone(f2));
|
||||
const formula* ftmp3 = unop::instance(unop::Not,
|
||||
(n == 0)? clone(f1) : clone(f2));
|
||||
const formula* ftmp4 = spot::ltl::negative_normal_form((n == 0)? f2 : f1);
|
||||
const formula* ftmp5;
|
||||
const formula* ftmp6;
|
||||
bool retour;
|
||||
|
||||
|
||||
ftmp2 = spot::ltl::unabbreviate_logic(ftmp3);
|
||||
ftmp1 = spot::ltl::negative_normal_form(ftmp2);
|
||||
|
||||
|
||||
ftmp5 = spot::ltl::unabbreviate_logic(ftmp4);
|
||||
ftmp6 = spot::ltl::negative_normal_form(ftmp5);
|
||||
|
||||
|
||||
if (n == 0)
|
||||
retour = inf_form(ftmp1, ftmp6);
|
||||
else
|
||||
else
|
||||
retour = inf_form(ftmp6, ftmp1);
|
||||
|
||||
|
||||
spot::ltl::destroy(ftmp1);
|
||||
spot::ltl::destroy(ftmp2);
|
||||
spot::ltl::destroy(ftmp3);
|
||||
spot::ltl::destroy(ftmp4);
|
||||
spot::ltl::destroy(ftmp5);
|
||||
spot::ltl::destroy(ftmp6);
|
||||
|
||||
|
||||
return retour;
|
||||
}
|
||||
|
||||
|
|
|
|||
28
src/sanity/80columns.test
Executable file
28
src/sanity/80columns.test
Executable file
|
|
@ -0,0 +1,28 @@
|
|||
#! /bin/sh
|
||||
|
||||
# Check that all files use at most 80 columns.
|
||||
|
||||
set -e
|
||||
|
||||
rm -f failures
|
||||
|
||||
find "${INCDIR-..}" \( -name "${1-*}.hh" -o -name "${1-*}.cc" \
|
||||
-o -name "${1-*}.test" \) -a -type f -a -print |
|
||||
while read file; do
|
||||
x='.........................................'
|
||||
if grep -q $x$x "$file"; then
|
||||
if grep 'GNU Bison' "$file" >/dev/null ||
|
||||
grep 'generated by flex' "$file" >/dev/null ; then
|
||||
:
|
||||
else
|
||||
echo "$file" >>failures
|
||||
fi
|
||||
fi
|
||||
done
|
||||
|
||||
if test -f failures; then
|
||||
echo "The following files contain lines with more than 80 characters:"
|
||||
cat failures
|
||||
rm failures
|
||||
exit 1;
|
||||
fi
|
||||
|
|
@ -30,6 +30,8 @@ check-local:
|
|||
CXXFLAGS='$(AM_CXXFLAGS) $(CXXFLAGS)' \
|
||||
INCDIR='$(top_srcdir)/src' \
|
||||
$(SHELL) $(srcdir)/includes.test $(TESTHEADER)
|
||||
INCDIR='$(top_srcdir)/src' \
|
||||
$(SHELL) $(srcdir)/80columns.test $(TESTHEADER)
|
||||
|
||||
# Ensure we have not forgotten to include an header.
|
||||
installcheck-local:
|
||||
|
|
|
|||
|
|
@ -47,7 +47,8 @@ run 0 ./explprod input1 input2 > stdout
|
|||
|
||||
# Sort out some possible inversions in the output.
|
||||
# (The order is not guaranteed by SPOT.)
|
||||
perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g;s/\(!b & a\)/(a & !b)/g;s/\(b & !a\)/(!a & b)/g' \
|
||||
perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g;
|
||||
s/\(!b & a\)/(a & !b)/g;s/\(b & !a\)/(!a & b)/g' \
|
||||
stdout > tmp_ && mv tmp_ stdout
|
||||
|
||||
cat stdout
|
||||
|
|
|
|||
|
|
@ -47,7 +47,8 @@ run 0 ./explprod input1 input2 > stdout
|
|||
|
||||
# Sort out some possible inversions in the output.
|
||||
# (The order is not guaranteed by SPOT.)
|
||||
sed 's/"p3" "p2"/"p2" "p3"/g;s/(!b & a)/(a \& !b)/g;s/(b & !a)/(!a \& b)/g' stdout > tmp_ && mv tmp_ stdout
|
||||
sed 's/"p3" "p2"/"p2" "p3"/g;s/(!b & a)/(a \& !b)/g;
|
||||
s/(b & !a)/(!a \& b)/g' stdout > tmp_ && mv tmp_ stdout
|
||||
|
||||
cat stdout
|
||||
diff stdout expected
|
||||
|
|
|
|||
|
|
@ -49,7 +49,8 @@ EOF
|
|||
run 0 ./explprod input1 input2 > stdout
|
||||
# Sort out some possible inversions in the output.
|
||||
# (The order is not guaranteed by SPOT.)
|
||||
perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g;s/\(c & a\)/(a & c)/g;s/\(b & a\)/(a & b)/g' \
|
||||
perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?/@{[sort $1, $2, $3]}/g;
|
||||
s/\(c & a\)/(a & c)/g;s/\(b & a\)/(a & b)/g' \
|
||||
stdout > tmp_ && mv tmp_ stdout
|
||||
|
||||
cat stdout
|
||||
|
|
|
|||
|
|
@ -185,7 +185,8 @@ Algorithm
|
|||
Algorithm
|
||||
{
|
||||
Name = "Spot (Couvreur -- FM exprop), fake, LTL simplifications by ltl2ba"
|
||||
Path = "${LBTT_TRANSLATE} --spot '${srcdir}/ltl2baw.pl --spot=\"-f -x -T\" -F'"
|
||||
Path =
|
||||
"${LBTT_TRANSLATE} --spot '${srcdir}/ltl2baw.pl --spot=\"-f -x -T\" -F'"
|
||||
Enabled = no
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -61,7 +61,8 @@ run 0 ./tripprod input1 input2 input3 > stdout
|
|||
|
||||
# Sort out some possible inversions in the output.
|
||||
# (The order is not guaranteed by SPOT.)
|
||||
perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?(?: ("\w+"))?/@{[sort $1, $2, $3, $4]}/g;s/\(c & a\)/(a & c)/g;s/\(b & a\)/(a & b)/g' \
|
||||
perl -pe 's/("\w+") ("\w+")(?: ("\w+"))?(?: ("\w+"))?/@{[sort $1,$2,$3,$4]}/g;
|
||||
s/\(c & a\)/(a & c)/g;s/\(b & a\)/(a & b)/g' \
|
||||
stdout > tmp_ &&
|
||||
mv tmp_ stdout
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue