Speedup reduccmp.test
This test used to take more than 10min because an instance of valgrind was launched for each separate equivalence check. The list of equivalences to checks are not given in a file, and only two valgrind instances are run. The test takes less than 15sec. * src/ltltest/equalsf.cc: New file. * src/ltltest/Makefile.am (reduccmp, reductaustr): Build using equalsf.cc. * src/ltltest/reduccmp.test: Rewrite. * src/ltltest/uwrm.test: Also rewrite, and use valgrind.
This commit is contained in:
Alexandre Duret-Lutz
parent
b43f75e917
commit
7b9f695265
4 changed files with 597 additions and 354 deletions
|
|
@ -60,13 +60,13 @@ lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DLUNABBREV
|
|||
nenoform_SOURCES = equals.cc
|
||||
nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM
|
||||
reduc_SOURCES = reduc.cc
|
||||
reduccmp_SOURCES = equals.cc
|
||||
reduccmp_SOURCES = equalsf.cc
|
||||
reduccmp_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC
|
||||
reduceu_SOURCES = equals.cc
|
||||
reduceu_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC -DEVENT_UNIV
|
||||
reductau_SOURCES = equals.cc
|
||||
reductau_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAU
|
||||
reductaustr_SOURCES = equals.cc
|
||||
reductaustr_SOURCES = equalsf.cc
|
||||
reductaustr_CPPFLAGS = $(AM_CPPFLAGS) -DREDUC_TAUSTR
|
||||
syntimpl_SOURCES = syntimpl.cc
|
||||
tostring_SOURCES = tostring.cc
|
||||
|
|
|
|||
251
src/ltltest/equalsf.cc
Normal file
251
src/ltltest/equalsf.cc
Normal file
|
|
@ -0,0 +1,251 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2014 Laboratoire de
|
||||
// Recherche et Développement de l'Epita (LRDE).
|
||||
// Copyright (C) 2003, 2004, 2006 Laboratoire d'Informatique de
|
||||
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
|
||||
// Université Pierre et Marie Curie.
|
||||
//
|
||||
// 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 3 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 this program. If not, see <http://www.gnu.org/licenses/>.
|
||||
|
||||
#include <iostream>
|
||||
#include <fstream>
|
||||
#include <sstream>
|
||||
#include <cassert>
|
||||
#include <cstdlib>
|
||||
#include <cstring>
|
||||
#include "ltlparse/public.hh"
|
||||
#include "ltlvisit/lunabbrev.hh"
|
||||
#include "ltlvisit/tunabbrev.hh"
|
||||
#include "ltlvisit/dump.hh"
|
||||
#include "ltlvisit/wmunabbrev.hh"
|
||||
#include "ltlvisit/nenoform.hh"
|
||||
#include "ltlast/allnodes.hh"
|
||||
#include "ltlvisit/simplify.hh"
|
||||
#include "ltlvisit/tostring.hh"
|
||||
|
||||
void
|
||||
syntax(char* prog)
|
||||
{
|
||||
std::cerr << prog << " [-E] file" << std::endl;
|
||||
exit(2);
|
||||
}
|
||||
|
||||
int
|
||||
main(int argc, char** argv)
|
||||
{
|
||||
bool check_first = true;
|
||||
|
||||
if (argc > 1 && !strcmp(argv[1], "-E"))
|
||||
{
|
||||
check_first = false;
|
||||
argv[1] = argv[0];
|
||||
++argv;
|
||||
--argc;
|
||||
}
|
||||
if (argc != 2)
|
||||
syntax(argv[0]);
|
||||
std::ifstream input(argv[1]);
|
||||
|
||||
std::string s;
|
||||
unsigned line = 0;
|
||||
while (std::getline(input, s))
|
||||
{
|
||||
++line;
|
||||
std::cerr << line << ": " << s << '\n';
|
||||
if (s[0] == '#') // Skip comments
|
||||
continue;
|
||||
std::vector<std::string> formulas;
|
||||
{
|
||||
std::istringstream ss(s);
|
||||
std::string form;
|
||||
while (std::getline(ss, form, ','))
|
||||
formulas.push_back(form);
|
||||
}
|
||||
|
||||
unsigned size = formulas.size();
|
||||
if (size == 0) // Skip empty lines
|
||||
continue;
|
||||
|
||||
if (size == 1)
|
||||
{
|
||||
std::cerr << "Not enough formulas on line " << line << '\n';
|
||||
return 2;
|
||||
}
|
||||
|
||||
spot::ltl::parse_error_list p2;
|
||||
const spot::ltl::formula* f2 = spot::ltl::parse(formulas[size - 1], p2);
|
||||
|
||||
if (spot::ltl::format_parse_errors(std::cerr, formulas[size - 1], p2))
|
||||
return 2;
|
||||
|
||||
for (unsigned n = 0; n < size - 1; ++n)
|
||||
{
|
||||
|
||||
spot::ltl::parse_error_list p1;
|
||||
const spot::ltl::formula* f1 = spot::ltl::parse(formulas[n], p1);
|
||||
|
||||
if (check_first &&
|
||||
spot::ltl::format_parse_errors(std::cerr, formulas[n], p1))
|
||||
return 2;
|
||||
|
||||
int exit_code = 0;
|
||||
|
||||
{
|
||||
#if defined LUNABBREV || defined TUNABBREV || defined NENOFORM || defined WM
|
||||
const spot::ltl::formula* tmp;
|
||||
#endif
|
||||
#ifdef LUNABBREV
|
||||
tmp = f1;
|
||||
f1 = spot::ltl::unabbreviate_logic(f1);
|
||||
tmp->destroy();
|
||||
spot::ltl::dump(std::cout, f1);
|
||||
std::cout << std::endl;
|
||||
#endif
|
||||
#ifdef TUNABBREV
|
||||
tmp = f1;
|
||||
f1 = spot::ltl::unabbreviate_ltl(f1);
|
||||
tmp->destroy();
|
||||
spot::ltl::dump(std::cout, f1);
|
||||
std::cout << std::endl;
|
||||
#endif
|
||||
#ifdef WM
|
||||
tmp = f1;
|
||||
f1 = spot::ltl::unabbreviate_wm(f1);
|
||||
tmp->destroy();
|
||||
spot::ltl::dump(std::cout, f1);
|
||||
std::cout << std::endl;
|
||||
#endif
|
||||
#ifdef NENOFORM
|
||||
tmp = f1;
|
||||
f1 = spot::ltl::negative_normal_form(f1);
|
||||
tmp->destroy();
|
||||
spot::ltl::dump(std::cout, f1);
|
||||
std::cout << std::endl;
|
||||
#endif
|
||||
#ifdef REDUC
|
||||
spot::ltl::ltl_simplifier_options opt(true, true, true,
|
||||
false, false);
|
||||
# ifdef EVENT_UNIV
|
||||
opt.favor_event_univ = true;
|
||||
# endif
|
||||
spot::ltl::ltl_simplifier simp(opt);
|
||||
{
|
||||
const spot::ltl::formula* tmp;
|
||||
tmp = f1;
|
||||
f1 = simp.simplify(f1);
|
||||
|
||||
if (!simp.are_equivalent(f1, tmp))
|
||||
{
|
||||
std::cerr
|
||||
<< "Source and simplified formulae are not equivalent!\n";
|
||||
std::cerr
|
||||
<< "Simplified: " << spot::ltl::to_string(f1) << '\n';
|
||||
exit_code = 1;
|
||||
}
|
||||
|
||||
tmp->destroy();
|
||||
}
|
||||
spot::ltl::dump(std::cout, f1);
|
||||
std::cout << std::endl;
|
||||
#endif
|
||||
#ifdef REDUC_TAU
|
||||
spot::ltl::ltl_simplifier_options opt(false, false, false,
|
||||
true, false);
|
||||
spot::ltl::ltl_simplifier simp(opt);
|
||||
{
|
||||
const spot::ltl::formula* tmp;
|
||||
tmp = f1;
|
||||
f1 = simp.simplify(f1);
|
||||
|
||||
if (!simp.are_equivalent(f1, tmp))
|
||||
{
|
||||
std::cerr
|
||||
<< "Source and simplified formulae are not equivalent!\n";
|
||||
std::cerr
|
||||
<< "Simplified: " << spot::ltl::to_string(f1) << '\n';
|
||||
exit_code = 1;
|
||||
}
|
||||
|
||||
tmp->destroy();
|
||||
}
|
||||
spot::ltl::dump(std::cout, f1);
|
||||
std::cout << std::endl;
|
||||
#endif
|
||||
#ifdef REDUC_TAUSTR
|
||||
spot::ltl::ltl_simplifier_options opt(false, false, false,
|
||||
true, true);
|
||||
spot::ltl::ltl_simplifier simp(opt);
|
||||
{
|
||||
const spot::ltl::formula* tmp;
|
||||
tmp = f1;
|
||||
f1 = simp.simplify(f1);
|
||||
|
||||
if (!simp.are_equivalent(f1, tmp))
|
||||
{
|
||||
std::cerr
|
||||
<< "Source and simplified formulae are not equivalent!\n";
|
||||
std::cerr
|
||||
<< "Simplified: " << spot::ltl::to_string(f1) << '\n';
|
||||
exit_code = 1;
|
||||
}
|
||||
|
||||
tmp->destroy();
|
||||
}
|
||||
spot::ltl::dump(std::cout, f1);
|
||||
std::cout << std::endl;
|
||||
#endif
|
||||
|
||||
exit_code |= f1 != f2;
|
||||
|
||||
#if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
|
||||
spot::ltl::ltl_simplifier simp;
|
||||
#endif
|
||||
|
||||
if (!simp.are_equivalent(f1, f2))
|
||||
{
|
||||
#if (!defined(REDUC) && !defined(REDUC_TAU) && !defined(REDUC_TAUSTR))
|
||||
std::cerr
|
||||
<< "Source and destination formulae are not equivalent!\n";
|
||||
#else
|
||||
std::cerr
|
||||
<< "Simpl. and destination formulae are not equivalent!\n";
|
||||
#endif
|
||||
exit_code = 1;
|
||||
}
|
||||
|
||||
if (exit_code)
|
||||
{
|
||||
spot::ltl::dump(std::cerr, f1) << std::endl;
|
||||
spot::ltl::dump(std::cerr, f2) << std::endl;
|
||||
return exit_code;
|
||||
}
|
||||
|
||||
}
|
||||
f1->destroy();
|
||||
}
|
||||
f2->destroy();
|
||||
}
|
||||
|
||||
spot::ltl::atomic_prop::dump_instances(std::cerr);
|
||||
spot::ltl::unop::dump_instances(std::cerr);
|
||||
spot::ltl::binop::dump_instances(std::cerr);
|
||||
spot::ltl::multop::dump_instances(std::cerr);
|
||||
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;
|
||||
}
|
||||
|
|
@ -25,368 +25,373 @@
|
|||
# Check LTL reductions
|
||||
|
||||
. ./defs || exit 1
|
||||
set -e
|
||||
|
||||
for x in ../reduccmp ../reductaustr; do
|
||||
cat >common.txt <<EOF
|
||||
# No reduction
|
||||
a U b, a U b
|
||||
a R b, a R b
|
||||
a & b, a & b
|
||||
a | b, a | b
|
||||
a & (a U b), a & (a U b)
|
||||
a | (a U b), a | (a U b)
|
||||
|
||||
# No reduction
|
||||
run 0 $x 'a U b' 'a U b'
|
||||
run 0 $x 'a R b' 'a R b'
|
||||
run 0 $x 'a & b' 'a & b'
|
||||
run 0 $x 'a | b' 'a | b'
|
||||
run 0 $x 'a & (a U b)' 'a & (a U b)'
|
||||
run 0 $x 'a | (a U b)' 'a | (a U b)'
|
||||
# Syntactic reduction
|
||||
a & (!b R !a), false
|
||||
(!b R !a) & a, false
|
||||
a & (!b R !a) & c, false
|
||||
c & (!b R !a) & a, false
|
||||
|
||||
# Syntactic reduction
|
||||
run 0 $x 'a & (!b R !a)' 'false'
|
||||
run 0 $x '(!b R !a) & a' 'false'
|
||||
run 0 $x 'a & (!b R !a) & c' 'false'
|
||||
run 0 $x 'c & (!b R !a) & a' 'false'
|
||||
a & (!b M !a), false
|
||||
(!b M !a) & a, false
|
||||
a & (!b M !a) & c, false
|
||||
c & (!b M !a) & a, false
|
||||
|
||||
run 0 $x 'a & (!b M !a)' 'false'
|
||||
run 0 $x '(!b M !a) & a' 'false'
|
||||
run 0 $x 'a & (!b M !a) & c' 'false'
|
||||
run 0 $x 'c & (!b M !a) & a' 'false'
|
||||
a & (b U a), a
|
||||
(b U a) & a, a
|
||||
a | (b U a), (b U a)
|
||||
(b U a) | a, (b U a)
|
||||
a U (b U a), (b U a)
|
||||
|
||||
run 0 $x 'a & (b U a)' 'a'
|
||||
run 0 $x '(b U a) & a' 'a'
|
||||
run 0 $x 'a | (b U a)' '(b U a)'
|
||||
run 0 $x '(b U a) | a' '(b U a)'
|
||||
run 0 $x 'a U (b U a)' '(b U a)'
|
||||
a & (b W a), a
|
||||
(b W a) & a, a
|
||||
a | (b W a), (b W a)
|
||||
(b W a) | a, (b W a)
|
||||
a W (b W a), (b W a)
|
||||
|
||||
run 0 $x 'a & (b W a)' 'a'
|
||||
run 0 $x '(b W a) & a' 'a'
|
||||
run 0 $x 'a | (b W a)' '(b W a)'
|
||||
run 0 $x '(b W a) | a' '(b W a)'
|
||||
run 0 $x 'a W (b W a)' '(b W a)'
|
||||
a & (b U a) & a, a
|
||||
a & (b U a) & a, a
|
||||
a | (b U a) | a, (b U a)
|
||||
a | (b U a) | a, (b U a)
|
||||
a U (b U a), (b U a)
|
||||
|
||||
run 0 $x 'a & (b U a) & a' 'a'
|
||||
run 0 $x 'a & (b U a) & a' 'a'
|
||||
run 0 $x 'a | (b U a) | a' '(b U a)'
|
||||
run 0 $x 'a | (b U a) | a' '(b U a)'
|
||||
run 0 $x 'a U (b U a)' '(b U a)'
|
||||
a & c & (b W a), a & c
|
||||
a & d & c & e & f & g & b & (x W (g & f)), a&b&c&d&e&f&g
|
||||
(F!a & X(!b R a)) | (Ga & X(b U !a)), F!a & X(!b R a)
|
||||
d & ((!a & d) | (a & d)), (!a & d) | (a & d)
|
||||
|
||||
run 0 $x 'a & c & (b W a)' 'a & c'
|
||||
run 0 $x 'a & d & c & e & f & g & b & (x W (g & f))' 'a&b&c&d&e&f&g'
|
||||
run 0 $x '(F!a & X(!b R a)) | (Ga & X(b U !a))' 'F!a & X(!b R a)'
|
||||
run 0 $x 'd & ((!a & d) | (a & d))' '(!a & d) | (a & d)'
|
||||
a <-> !a, 0
|
||||
a <-> a, 1
|
||||
a ^ a, 0
|
||||
a ^ !a, 1
|
||||
|
||||
run 0 $x 'a <-> !a' '0'
|
||||
run 0 $x 'a <-> a' '1'
|
||||
run 0 $x 'a ^ a' '0'
|
||||
run 0 $x 'a ^ !a' '1'
|
||||
GFa | FGa, GFa
|
||||
XXGa | GFa, GFa
|
||||
GFa & FGa, FGa
|
||||
XXGa & GFa, XXGa
|
||||
|
||||
run 0 $x 'GFa | FGa' 'GFa'
|
||||
run 0 $x 'XXGa | GFa' 'GFa'
|
||||
run 0 $x 'GFa & FGa' 'FGa'
|
||||
run 0 $x 'XXGa & GFa' 'XXGa'
|
||||
# Basic reductions
|
||||
X(true), true
|
||||
X(false), false
|
||||
F(true), true
|
||||
F(false), false
|
||||
|
||||
# Basic reductions
|
||||
run 0 $x 'X(true)' 'true'
|
||||
run 0 $x 'X(false)' 'false'
|
||||
run 0 $x 'F(true)' 'true'
|
||||
run 0 $x 'F(false)' 'false'
|
||||
XGF(f), GF(f)
|
||||
|
||||
run 0 $x 'XGF(f)' 'GF(f)'
|
||||
# not reduced
|
||||
a R (b W G(c)), a R (b W G(c))
|
||||
# not reduced.
|
||||
a M ((a&b) R c), a M ((a&b) R c)
|
||||
# not reduced.
|
||||
(a&b) W (a U c), (a&b) W (a U c)
|
||||
|
||||
case $x in
|
||||
*tau*);;
|
||||
*)
|
||||
run 0 $x 'G(true)' 'true'
|
||||
run 0 $x 'G(false)' 'false'
|
||||
# Eventuality and universality class reductions
|
||||
FFa, Fa
|
||||
FGFa, GFa
|
||||
b U Fa, Fa
|
||||
b U GFa, GFa
|
||||
Ga, Ga
|
||||
|
||||
run 0 $x 'a M 1' 'Fa'
|
||||
run 0 $x 'a W 0' 'Ga'
|
||||
run 0 $x '1 U a' 'Fa'
|
||||
run 0 $x '0 R a' 'Ga'
|
||||
a U XXXFb, XXXFb
|
||||
EOF
|
||||
|
||||
run 0 $x 'G(a R b)' 'G(b)'
|
||||
cp common.txt nottau.txt
|
||||
cat >>nottau.txt<<EOF
|
||||
G(true), true
|
||||
G(false), false
|
||||
|
||||
run 0 $x 'FX(a)' 'XF(a)'
|
||||
run 0 $x 'GX(a)' 'XG(a)'
|
||||
a M 1, Fa
|
||||
a W 0, Ga
|
||||
1 U a, Fa
|
||||
0 R a, Ga
|
||||
|
||||
run 0 $x '(Xf W 0) | X(f W 0)' 'XGf'
|
||||
run 0 $x 'XFa & FXa' 'XFa'
|
||||
G(a R b), G(b)
|
||||
|
||||
run 0 $x 'GF(a | Xb)' 'GF(a | b)'
|
||||
run 0 $x 'GF(a | Fb)' 'GF(a | b)'
|
||||
run 0 $x 'GF(Xa | Fb)' 'GF(a | b)'
|
||||
run 0 $x 'FG(a & Xb)' 'FG(a & b)'
|
||||
run 0 $x 'FG(a & Gb)' 'FG(a & b)'
|
||||
run 0 $x 'FG(Xa & Gb)' 'FG(a & b)'
|
||||
FX(a), XF(a)
|
||||
GX(a), XG(a)
|
||||
|
||||
run 0 $x 'X(a) U X(b)' 'X(a U b)'
|
||||
run 0 $x 'X(a) R X(b)' 'X(a R b)'
|
||||
run 0 $x 'Xa & Xb' 'X(a & b)'
|
||||
run 0 $x 'Xa | Xb' 'X(a | b)'
|
||||
(Xf W 0) | X(f W 0), XGf
|
||||
XFa & FXa, XFa
|
||||
|
||||
run 0 $x 'X(a) M X(b)' 'X(a M b)'
|
||||
run 0 $x 'X(a) W X(b)' 'X(a W b)'
|
||||
run 0 $x 'X(a) M b' 'b & X(b U a)'
|
||||
run 0 $x 'X(a) R b' 'b & X(b W a)'
|
||||
run 0 $x 'X(a) U b' 'b | X(b M a)'
|
||||
run 0 $x 'X(a) W b' 'b | X(b R a)'
|
||||
GF(a | Xb), GF(a | b)
|
||||
GF(a | Fb), GF(a | b)
|
||||
GF(Xa | Fb), GF(a | b)
|
||||
FG(a & Xb), FG(a & b)
|
||||
FG(a & Gb), FG(a & b)
|
||||
FG(Xa & Gb), FG(a & b)
|
||||
|
||||
run 0 $x '(a U b) & (c U b)' '(a & c) U b'
|
||||
run 0 $x '(a R b) & (a R c)' 'a R (b & c)'
|
||||
run 0 $x '(a U b) | (a U c)' 'a U (b | c)'
|
||||
run 0 $x '(a R b) | (c R b)' '(a | c) R b'
|
||||
X(a) U X(b), X(a U b)
|
||||
X(a) R X(b), X(a R b)
|
||||
Xa & Xb, X(a & b)
|
||||
Xa | Xb, X(a | b)
|
||||
|
||||
run 0 $x 'Xa & FGb' 'X(a & FGb)'
|
||||
run 0 $x 'Xa | FGb' 'X(a | FGb)'
|
||||
run 0 $x 'Xa & GFb' 'X(a & GFb)'
|
||||
run 0 $x 'Xa | GFb' 'X(a | GFb)'
|
||||
# The following is not reduced to F(a) & GFb. because
|
||||
# (1) is does not help the translate the formula into a
|
||||
# smaller automaton, and ...
|
||||
run 0 $x 'F(a & GFb)' 'F(a & GFb)'
|
||||
# (2) ... it would hinder this useful reduction (that helps to
|
||||
# produce a smaller automaton)
|
||||
run 0 $x 'F(f1 & GF(f2)) | F(a & GF(b))' 'F((f1&GFf2)|(a&GFb))'
|
||||
# FIXME: Don't we want the opposite rewriting?
|
||||
# rewriting Fa & GFb as F(a & GFb) seems better, but
|
||||
# it not clear how that scales to Fa & Fb & GFc...
|
||||
run 0 $x 'Fa & GFb' 'Fa & GFb'
|
||||
run 0 $x 'G(a | GFb)' 'Ga | GFb'
|
||||
# The following is not reduced to F(a & c) & GF(b) for the same
|
||||
# reason as above.
|
||||
run 0 $x 'F(a & GFb & c)' 'F(a & GFb & c)'
|
||||
run 0 $x 'G(a | GFb | c)' 'G(a | c) | GFb'
|
||||
X(a) M X(b), X(a M b)
|
||||
X(a) W X(b), X(a W b)
|
||||
X(a) M b, b & X(b U a)
|
||||
X(a) R b, b & X(b W a)
|
||||
X(a) U b, b | X(b M a)
|
||||
X(a) W b, b | X(b R a)
|
||||
|
||||
run 0 $x 'GFa <=> GFb' 'G(Fa&Fb)|FG(!a&!b)'
|
||||
(a U b) & (c U b), (a & c) U b
|
||||
(a R b) & (a R c), a R (b & c)
|
||||
(a U b) | (a U c), a U (b | c)
|
||||
(a R b) | (c R b), (a | c) R b
|
||||
|
||||
run 0 $x 'Gb W a' 'Gb|a'
|
||||
run 0 $x 'Fb M Fa' 'Fa & Fb'
|
||||
Xa & FGb, X(a & FGb)
|
||||
Xa | FGb, X(a | FGb)
|
||||
Xa & GFb, X(a & GFb)
|
||||
Xa | GFb, X(a | GFb)
|
||||
# The following is not reduced to F(a) & GFb. because
|
||||
# (1) is does not help the translate the formula into a
|
||||
# smaller automaton, and ...
|
||||
F(a & GFb), F(a & GFb)
|
||||
# (2) ... it would hinder this useful reduction (that helps to
|
||||
# produce a smaller automaton)
|
||||
F(f1 & GF(f2)) | F(a & GF(b)), F((f1&GFf2)|(a&GFb))
|
||||
# FIXME: Don't we want the opposite rewriting?
|
||||
# rewriting Fa & GFb as F(a & GFb) seems better, but
|
||||
# it not clear how that scales to Fa & Fb & GFc...
|
||||
Fa & GFb, Fa & GFb
|
||||
G(a | GFb), Ga | GFb
|
||||
# The following is not reduced to F(a & c) & GF(b) for the same
|
||||
# reason as above.
|
||||
F(a & GFb & c), F(a & GFb & c)
|
||||
G(a | GFb | c), G(a | c) | GFb
|
||||
|
||||
run 0 $x 'a U (b | G(a) | c)' 'a W (b | c)'
|
||||
run 0 $x 'a U (G(a))' 'Ga'
|
||||
run 0 $x '(a U b) | (a W c)' 'a W (b | c)'
|
||||
run 0 $x '(a U b) | Ga' 'a W b'
|
||||
GFa <=> GFb, G(Fa&Fb)|FG(!a&!b)
|
||||
|
||||
run 0 $x 'a R (b & F(a) & c)' 'a M (b & c)'
|
||||
run 0 $x 'a R (F(a))' 'Fa'
|
||||
run 0 $x '(a R b) & (a M c)' 'a M (b & c)'
|
||||
run 0 $x '(a R b) & Fa' 'a M b'
|
||||
Gb W a, Gb|a
|
||||
Fb M Fa, Fa & Fb
|
||||
|
||||
run 0 $x '(a U b) & (c W b)' '(a & c) U b'
|
||||
run 0 $x '(a W b) & (c W b)' '(a & c) W b'
|
||||
run 0 $x '(a R b) | (c M b)' '(a | c) R b'
|
||||
run 0 $x '(a M b) | (c M b)' '(a | c) M b'
|
||||
a U (b | G(a) | c), a W (b | c)
|
||||
a U (G(a)), Ga
|
||||
(a U b) | (a W c), a W (b | c)
|
||||
(a U b) | Ga, a W b
|
||||
|
||||
run 0 $x '(a R b) | Gb' 'a R b'
|
||||
run 0 $x '(a M b) | Gb' 'a R b'
|
||||
run 0 $x '(a U b) & Fb' 'a U b'
|
||||
run 0 $x '(a W b) & Fb' 'a U b'
|
||||
run 0 $x '(a M b) | Gb | (c M b)' '(a | c) R b'
|
||||
a R (b & F(a) & c), a M (b & c)
|
||||
a R (F(a)), Fa
|
||||
(a R b) & (a M c), a M (b & c)
|
||||
(a R b) & Fa, a M b
|
||||
|
||||
run 0 $x 'GFGa' 'FGa'
|
||||
run 0 $x 'b R Ga' 'Ga'
|
||||
run 0 $x 'b R FGa' 'FGa'
|
||||
(a U b) & (c W b), (a & c) U b
|
||||
(a W b) & (c W b), (a & c) W b
|
||||
(a R b) | (c M b), (a | c) R b
|
||||
(a M b) | (c M b), (a | c) M b
|
||||
|
||||
run 0 $x 'G(!a M a) M 1' '0'
|
||||
run 0 $x 'G(!a M a) U 1' '1'
|
||||
run 0 $x 'a R (!a M a)' '0'
|
||||
run 0 $x 'a W (!a M a)' 'Ga'
|
||||
(a R b) | Gb, a R b
|
||||
(a M b) | Gb, a R b
|
||||
(a U b) & Fb, a U b
|
||||
(a W b) & Fb, a U b
|
||||
(a M b) | Gb | (c M b), (a | c) R b
|
||||
|
||||
run 0 $x 'F(a U b)' 'Fb'
|
||||
run 0 $x 'F(a M b)' 'F(a & b)'
|
||||
run 0 $x 'G(a R b)' 'Gb'
|
||||
run 0 $x 'G(a W b)' 'G(a | b)'
|
||||
GFGa, FGa
|
||||
b R Ga, Ga
|
||||
b R FGa, FGa
|
||||
|
||||
run 0 $x 'Fa W Fb' 'F(GFa | b)'
|
||||
run 0 $x 'Ga M Gb' 'FGa & Gb'
|
||||
G(!a M a) M 1, 0
|
||||
G(!a M a) U 1, 1
|
||||
a R (!a M a), 0
|
||||
a W (!a M a), Ga
|
||||
|
||||
run 0 $x 'a & XGa' 'Ga'
|
||||
run 0 $x 'a & XG(a&b)' '(XGb)&(Ga)'
|
||||
run 0 $x 'a & b & XG(a&b)' 'G(a&b)'
|
||||
run 0 $x 'a & b & X(Ga&Gb)' 'G(a&b)'
|
||||
run 0 $x 'a & b & XGa &XG(b)' 'G(a&b)'
|
||||
run 0 $x 'a & b & XGa & XGc' 'b & Ga & XGc'
|
||||
run 0 $x 'a & b & X(G(a&d) & b) & X(Gc)' 'b & Ga & X(b & G(c&d))'
|
||||
run 0 $x 'a|b|c|X(F(a|b)|F(c)|Gd)' 'F(a|b|c)|XGd'
|
||||
run 0 $x 'b|c|X(F(a|b)|F(c)|Gd)' 'b|c|X(F(a|b|c)|Gd)'
|
||||
F(a U b), Fb
|
||||
F(a M b), F(a & b)
|
||||
G(a R b), Gb
|
||||
G(a W b), G(a | b)
|
||||
|
||||
run 0 $x 'a | (Xa R b) | c' '(b W a) | c'
|
||||
run 0 $x 'a | (Xa M b) | c' '(b U a) | c'
|
||||
run 0 $x 'a | (Xa M b) | (Xa R c)' '(b U a) | (c W a)'
|
||||
run 0 $x 'a | (Xa M b) | XF(a)' 'Fa'
|
||||
run 0 $x 'a | (Xa R b) | XF(a)' '(b W a) | Fa' # Gb | Fa ?
|
||||
run 0 $x 'a & (Xa W b) & c' '(b R a) & c'
|
||||
run 0 $x 'a & (Xa U b) & c' '(b M a) & c'
|
||||
run 0 $x 'a & (Xa W b) & (Xa U c)' '(b R a) & (c M a)'
|
||||
run 0 $x 'a & (Xa W b) & XGa' 'Ga'
|
||||
run 0 $x 'a & (Xa U b) & XGa' '(b M a) & Ga' # Fb & Ga ?
|
||||
run 0 $x 'a|(c&b&X((b&c) U a))|d' '((b&c) U a)|d'
|
||||
run 0 $x 'a|(c&X((b&c) W a)&b)|d' '((b&c) W a)|d'
|
||||
run 0 $x 'a&(c|b|X((b|c) M a))&d' '((b|c) M a)&d'
|
||||
run 0 $x 'a&(c|X((b|c) R a)|b)&d' '((b|c) R a)&d'
|
||||
run 0 $x 'g R (f|g|h)' '(f|h) W g'
|
||||
run 0 $x 'g M (f|g|h)' '(f|h) U g'
|
||||
run 0 $x 'g U (f&g&h)' '(f&h) M g'
|
||||
run 0 $x 'g W (f&g&h)' '(f&h) R g'
|
||||
Fa W Fb, F(GFa | b)
|
||||
Ga M Gb, FGa & Gb
|
||||
|
||||
# Syntactic implication
|
||||
run 0 $x '(a & b) R (a R c)' '(a & b)R c'
|
||||
run 0 $x 'a R ((a & b) R c)' '(a & b)R c'
|
||||
run 0 $x 'a R ((a & b) M c)' '(a & b)M c'
|
||||
run 0 $x 'a M ((a & b) M c)' '(a & b)M c'
|
||||
run 0 $x '(a & b) M (a R c)' '(a & b)M c'
|
||||
run 0 $x '(a & b) M (a M c)' '(a & b)M c'
|
||||
a & XGa, Ga
|
||||
a & XG(a&b), (XGb)&(Ga)
|
||||
a & b & XG(a&b), G(a&b)
|
||||
a & b & X(Ga&Gb), G(a&b)
|
||||
a & b & XGa &XG(b), G(a&b)
|
||||
a & b & XGa & XGc, b & Ga & XGc
|
||||
a & b & X(G(a&d) & b) & X(Gc), b & Ga & X(b & G(c&d))
|
||||
a|b|c|X(F(a|b)|F(c)|Gd), F(a|b|c)|XGd
|
||||
b|c|X(F(a|b)|F(c)|Gd), b|c|X(F(a|b|c)|Gd)
|
||||
|
||||
run 0 $x 'a U ((a & b) U c)' 'a U c'
|
||||
run 0 $x '(a&c) U (b R (c U d))' 'b R (c U d)'
|
||||
run 0 $x '(a&c) U (b R (c W d))' 'b R (c W d)'
|
||||
run 0 $x '(a&c) U (b M (c U d))' 'b M (c U d)'
|
||||
run 0 $x '(a&c) U (b M (c W d))' 'b M (c W d)'
|
||||
a | (Xa R b) | c, (b W a) | c
|
||||
a | (Xa M b) | c, (b U a) | c
|
||||
a | (Xa M b) | (Xa R c), (b U a) | (c W a)
|
||||
a | (Xa M b) | XF(a), Fa
|
||||
# Gb | Fa ?
|
||||
a | (Xa R b) | XF(a), (b W a) | Fa
|
||||
a & (Xa W b) & c, (b R a) & c
|
||||
a & (Xa U b) & c, (b M a) & c
|
||||
a & (Xa W b) & (Xa U c), (b R a) & (c M a)
|
||||
a & (Xa W b) & XGa, Ga
|
||||
# Fb & Ga ?
|
||||
a & (Xa U b) & XGa, (b M a) & Ga
|
||||
a|(c&b&X((b&c) U a))|d, ((b&c) U a)|d
|
||||
a|(c&X((b&c) W a)&b)|d, ((b&c) W a)|d
|
||||
a&(c|b|X((b|c) M a))&d, ((b|c) M a)&d
|
||||
a&(c|X((b|c) R a)|b)&d, ((b|c) R a)&d
|
||||
g R (f|g|h), (f|h) W g
|
||||
g M (f|g|h), (f|h) U g
|
||||
g U (f&g&h), (f&h) M g
|
||||
g W (f&g&h), (f&h) R g
|
||||
|
||||
run 0 $x '(a R c) R (b & a)' 'c R (b & a)'
|
||||
run 0 $x '(a M c) R (b & a)' 'c R (b & a)'
|
||||
# Syntactic implication
|
||||
(a & b) R (a R c), (a & b)R c
|
||||
a R ((a & b) R c), (a & b)R c
|
||||
a R ((a & b) M c), (a & b)M c
|
||||
a M ((a & b) M c), (a & b)M c
|
||||
(a & b) M (a R c), (a & b)M c
|
||||
(a & b) M (a M c), (a & b)M c
|
||||
|
||||
run 0 $x 'a W ((a&b) U c)' 'a W c'
|
||||
run 0 $x 'a W ((a&b) W c)' 'a W c'
|
||||
a U ((a & b) U c), a U c
|
||||
(a&c) U (b R (c U d)), b R (c U d)
|
||||
(a&c) U (b R (c W d)), b R (c W d)
|
||||
(a&c) U (b M (c U d)), b M (c U d)
|
||||
(a&c) U (b M (c W d)), b M (c W d)
|
||||
|
||||
run 0 $x '(a M c) M (b&a)' 'c M (b&a)'
|
||||
(a R c) R (b & a), c R (b & a)
|
||||
(a M c) R (b & a), c R (b & a)
|
||||
|
||||
run 0 $x '((a&c) U b) U c' 'b U c'
|
||||
run 0 $x '((a&c) W b) U c' 'b U c'
|
||||
run 0 $x '((a&c) U b) W c' 'b W c'
|
||||
run 0 $x '((a&c) W b) W c' 'b W c'
|
||||
run 0 $x '(a R b) R (c&a)' 'b R (c&a)'
|
||||
run 0 $x '(a M b) R (c&a)' 'b R (c&a)'
|
||||
run 0 $x '(a R b) M (c&a)' 'b M (c&a)'
|
||||
run 0 $x '(a M b) M (c&a)' 'b M (c&a)'
|
||||
a W ((a&b) U c), a W c
|
||||
a W ((a&b) W c), a W c
|
||||
|
||||
run 0 $x '(a R (b&c)) R (c)' '(a&b&c) R c'
|
||||
run 0 $x '(a M (b&c)) R (c)' '(a&b&c) R c'
|
||||
run 0 $x '(a R (b&c)) M (c)' '(a R (b&c)) M (c)' # not reduced
|
||||
run 0 $x '(a M (b&c)) M (c)' '(a&b&c) M c'
|
||||
run 0 $x '(a W (c&b)) W b' '(a W (c&b)) | b'
|
||||
run 0 $x '(a U (c&b)) W b' '(a U (c&b)) | b'
|
||||
run 0 $x '(a U (c&b)) U b' '(a U (c&b)) | b'
|
||||
run 0 $x '(a W (c&b)) U b' '(a W (c&b)) U b' # not reduced
|
||||
(a M c) M (b&a), c M (b&a)
|
||||
|
||||
((a&c) U b) U c, b U c
|
||||
((a&c) W b) U c, b U c
|
||||
((a&c) U b) W c, b W c
|
||||
((a&c) W b) W c, b W c
|
||||
(a R b) R (c&a), b R (c&a)
|
||||
(a M b) R (c&a), b R (c&a)
|
||||
(a R b) M (c&a), b M (c&a)
|
||||
(a M b) M (c&a), b M (c&a)
|
||||
|
||||
# Eventuality and universality class reductions
|
||||
run 0 $x 'Fa M b' 'Fa & b'
|
||||
run 0 $x 'GFa M b' 'GFa & b'
|
||||
(a R (b&c)) R (c), (a&b&c) R c
|
||||
(a M (b&c)) R (c), (a&b&c) R c
|
||||
# not reduced
|
||||
(a R (b&c)) M (c), (a R (b&c)) M (c)
|
||||
(a M (b&c)) M (c), (a&b&c) M c
|
||||
(a W (c&b)) W b, (a W (c&b)) | b
|
||||
(a U (c&b)) W b, (a U (c&b)) | b
|
||||
(a U (c&b)) U b, (a U (c&b)) | b
|
||||
# not reduced
|
||||
(a W (c&b)) U b, (a W (c&b)) U b
|
||||
|
||||
run 0 $x 'Fa|Xb|GFc' 'Fa | X(b|GFc)'
|
||||
run 0 $x 'Fa|GFc' 'F(a|GFc)'
|
||||
run 0 $x 'FGa|GFc' 'F(Ga|GFc)'
|
||||
run 0 $x 'Ga&Xb&FGc' 'Ga & X(b&FGc)'
|
||||
run 0 $x 'Ga&Xb&GFc' 'Ga & X(b&GFc)'
|
||||
run 0 $x 'Ga&GFc' 'G(a&Fc)'
|
||||
run 0 $x 'G(a|b|GFc|GFd|FGe|FGf)' 'G(a|b)|GF(c|d)|F(Ge|Gf)'
|
||||
run 0 $x 'G(a|b)|GFc|GFd|FGe|FGf' 'G(a|b)|GF(c|d)|F(Ge|Gf)'
|
||||
run 0 $x 'X(a|b)|GFc|GFd|FGe|FGf' 'X(a|b|GF(c|d)|F(Ge|Gf))'
|
||||
run 0 $x 'Xa&Xb&GFc&GFd&Ge' 'X(a&b&G(Fc&Fd))&Ge'
|
||||
# Eventuality and universality class reductions
|
||||
Fa M b, Fa & b
|
||||
GFa M b, GFa & b
|
||||
|
||||
# F comes in front when possible...
|
||||
run 0 $x 'GFc|GFd|FGe|FGf' 'F(GF(c|d)|Ge|Gf)'
|
||||
run 0 $x 'G(GFc|GFd|FGe|FGf)' 'F(GF(c|d)|Ge|Gf)'
|
||||
Fa|Xb|GFc, Fa | X(b|GFc)
|
||||
Fa|GFc, F(a|GFc)
|
||||
FGa|GFc, F(Ga|GFc)
|
||||
Ga&Xb&FGc, Ga & X(b&FGc)
|
||||
Ga&Xb&GFc, Ga & X(b&GFc)
|
||||
Ga&GFc, G(a&Fc)
|
||||
G(a|b|GFc|GFd|FGe|FGf), G(a|b)|GF(c|d)|F(Ge|Gf)
|
||||
G(a|b)|GFc|GFd|FGe|FGf, G(a|b)|GF(c|d)|F(Ge|Gf)
|
||||
X(a|b)|GFc|GFd|FGe|FGf, X(a|b|GF(c|d)|F(Ge|Gf))
|
||||
Xa&Xb&GFc&GFd&Ge, X(a&b&G(Fc&Fd))&Ge
|
||||
|
||||
# Because reduccmp will translate the formula,
|
||||
# this also check for an old bug in ltl2tgba_fm.
|
||||
run 0 $x '{(c&!c)[->0..1]}!' '0'
|
||||
# F comes in front when possible...
|
||||
GFc|GFd|FGe|FGf, F(GF(c|d)|Ge|Gf)
|
||||
G(GFc|GFd|FGe|FGf), F(GF(c|d)|Ge|Gf)
|
||||
|
||||
# Tricky case that used to break the translator,
|
||||
# because it was translating closer on-the-fly
|
||||
# without pruning the rational automaton.
|
||||
run 0 $x '{(c&!c)[=2]}' '0'
|
||||
# Because reduccmp will translate the formula,
|
||||
# this also check for an old bug in ltl2tgba_fm.
|
||||
{(c&!c)[->0..1]}!, 0
|
||||
|
||||
run 0 $x '{a && b && c*} <>-> d' 'a&b&c&d'
|
||||
run 0 $x '{a && b && c[*1..3]} <>-> d' 'a&b&c&d'
|
||||
run 0 $x '{a && b && c[->0..2]} <>-> d' 'a&b&c&d'
|
||||
run 0 $x '{a && b && c[+]} <>-> d' 'a&b&c&d'
|
||||
run 0 $x '{a && b && c[=1]} <>-> d' 'a&b&c&d'
|
||||
run 0 $x '{a && b && d[=2]} <>-> d' '0'
|
||||
run 0 $x '{a && b && d[*2..]} <>-> d' '0'
|
||||
run 0 $x '{a && b && d[->2..4]} <>-> d' '0'
|
||||
run 0 $x '{a && { c* : b* : (g|h)*}} <>-> d' 'a & c & b & (g | h) & d'
|
||||
run 0 $x '{a && {b;c}} <>-> d' '0'
|
||||
run 0 $x '{a && {(b;c):e}} <>-> d' '0'
|
||||
run 0 $x '{a && {b*;c*}} <>-> d' '{a && {b*|c*}} <>-> d' # until better
|
||||
run 0 $x '{a && {(b*;c*):e}} <>-> d' '{a && {b*|c*} && e} <>-> d' # idem
|
||||
run 0 $x '{a && {b*;c}} <>-> d' 'a & c & d'
|
||||
run 0 $x '{a && {(b*;c):e}} <>-> d' 'a & c & d & e'
|
||||
run 0 $x '{a && {b;c*}} <>-> d' 'a & b & d'
|
||||
run 0 $x '{a && {(b;c*):e}} <>-> d' 'a & b & d & e'
|
||||
run 0 $x '{{{b1;r1*}&&{b2;r2*}};c}' 'b1&b2&X{{r1*&&r2*};c}'
|
||||
run 0 $x '{{b1:r1*}&&{b2:r2*}}' '{{b1&&b2}:{r1*&&r2*}}'
|
||||
run 0 $x '{{r1*;b1}&&{r2*;b2}}' '{{r1*&&r2*};{b1&&b2}}'
|
||||
run 0 $x '{{r1*:b1}&&{r2*:b2}}' '{{r1*&&r2*}:{b1&&b2}}'
|
||||
run 0 $x '{{a;b*;c}&&{d;e*}&&{f*;g}&&{h*}}' \
|
||||
'{{f*;g}&&{h*}&&{{a&&d};{e* && {b*;c}}}}'
|
||||
run 0 $x '{{{b1;r1*}&{b2;r2*}};c}' 'b1&b2&X{{r1*&r2*};c}'
|
||||
run 0 $x '{{b1:(r1;x1*)}&{b2:(r2;x2*)}}' '{{b1&&b2}:{{r1&&r2};{x1*&x2*}}}'
|
||||
run 0 $x '{{b1:r1*}&{b2:r2*}}' '{{b1:r1*}&{b2:r2*}}' # Not reduced
|
||||
run 0 $x '{{r1*;b1}&{r2*;b2}}' '{{r1*;b1}&{r2*;b2}}' # Not reduced
|
||||
run 0 $x '{{r1*:b1}&{r2*:b2}}' '{{r1*:b1}&{r2*:b2}}' # Not reduced
|
||||
run 0 $x '{{a;b*;c}&{d;e*}&{f*;g}&{h*}}' \
|
||||
'{{f*;g}&{h*}&{{a&&d};{e* & {b*;c}}}}'
|
||||
run 0 $x '{a;(b*;c*;([*0]+{d;e}))*}!' '{a;{b|c|{d;e}}*}!'
|
||||
run 0 $x '{a&b&c*}|->!Xb' '(X!b | !(a & b)) & (!(a & b) | !c | X(!c R !b))'
|
||||
run 0 $x '{[*]}[]->b' 'Gb'
|
||||
run 0 $x '{a;[*]}[]->b' 'Gb | !a'
|
||||
run 0 $x '{[*];a}[]->b' 'G(b | !a)'
|
||||
run 0 $x '{a;b;[*]}[]->c' '!a | X(!b | Gc)'
|
||||
run 0 $x '{a;a;[*]}[]->c' '!a | X(!a | Gc)'
|
||||
run 0 $x '{s[*]}[]->b' 'b W !s'
|
||||
run 0 $x '{s[+]}[]->b' 'b W !s'
|
||||
run 0 $x '{s[*2..]}[]->b' '!s | X(b W !s)'
|
||||
run 0 $x '{a;b*;c;d*}[]->e' '!a | X(!b R ((e & X(e W !d)) | !c))'
|
||||
run 0 $x '{a:b*:c:d*}[]->e' '!a | ((!c | (e W !d)) W !b)'
|
||||
run 0 $x '{a|b*|c|d*}[]->e' '(e | !(a | c)) & (e W !b) & (e W !d)'
|
||||
run 0 $x '{{[*0] | a};b;{[*0] | a};c;e[*]} []-> f' \
|
||||
'{{[*0] | a};b;{[*0] | a}} []-> X((f & X(f W !e)) | !c)'
|
||||
# Tricky case that used to break the translator,
|
||||
# because it was translating closer on-the-fly
|
||||
# without pruning the rational automaton.
|
||||
{(c&!c)[=2]}, 0
|
||||
|
||||
run 0 $x '{a&b&c*}<>->!Xb' '(a & b & X!b) | (a & b & c & X(c U !b))'
|
||||
run 0 $x '{[*]}<>->b' 'Fb'
|
||||
run 0 $x '{a;[*]}<>->b' 'Fb & a'
|
||||
run 0 $x '{[*];a}<>->b' 'F(a & b)'
|
||||
run 0 $x '{a;b;[*]}<>->c' 'a & X(b & Fc)'
|
||||
run 0 $x '{a;a;[*]}<>->c' 'a & X(a & Fc)'
|
||||
run 0 $x '{s[*]}<>->b' 'b M s'
|
||||
run 0 $x '{s[+]}<>->b' 'b M s'
|
||||
run 0 $x '{s[*2..]}<>->b' 's & X(b M s)'
|
||||
run 0 $x '{1:a*}!' 'a'
|
||||
run 0 $x '{(1;1):a*}!' 'Xa'
|
||||
run 0 $x '{a;b*;c;d*}<>->e' 'a & X(b U (c & (e | X(e M d))))'
|
||||
run 0 $x '{a:b*:c:d*}<>->e' 'a & ((c & (e M d)) M b)'
|
||||
run 0 $x '{a|b*|c|d*}<>->e' '((a | c) & e) | (e M b) | (e M d)'
|
||||
run 0 $x '{{[*0] | a};b;{[*0] | a};c;e[*]} <>-> f' \
|
||||
'{{[*0] | a};b;{[*0] | a}} <>-> X(c & (f | X(f M e)))'
|
||||
run 0 $x '{a;b[*];c[*];e;f*}' 'a & X(b W (c W e))'
|
||||
run 0 $x '{a;b*;(a* && (b;c));c*}' 'a & X(b W {a[*] && {b;c}})'
|
||||
run 0 $x '{a;a;b[*2..];b}' 'a & X(a & X(b & X(b & Xb)))'
|
||||
run 0 $x '!{a;a;b[*2..];b}' '!a | X(!a | X(!b | X(!b | X!b)))'
|
||||
run 0 $x '!{a;b[*];c[*];e;f*}' '!a | X(!b M (!c M !e))'
|
||||
run 0 $x '!{a;b*;(a* && (b;c));c*}' '!a | X(!b M !{a[*] && {b;c}})'
|
||||
run 0 $x '{(a;c*;d)|(b;c)}' '(a & X(c W d)) | (b & Xc)'
|
||||
run 0 $x '!{(a;c*;d)|(b;c)}' '(X(!c M !d) | !a) & (X!c | !b)'
|
||||
run 0 $x '(Xc R b) & (Xc W 0)' 'b & XGc'
|
||||
run 0 $x '{{c*|1}[*0..1]}<>-> v' '{{c[+]|1}[*0..1]}<>-> v'
|
||||
run 0 $x '{{b*;c*}[*3..5]}<>-> v' '{{b*;c*}[*0..5]} <>-> v'
|
||||
run 0 $x '{{b*&c*}[*3..5]}<>-> v' '{{b[+]|c[+]}[*0..5]} <>-> v'
|
||||
{a && b && c*} <>-> d, a&b&c&d
|
||||
{a && b && c[*1..3]} <>-> d, a&b&c&d
|
||||
{a && b && c[->0..2]} <>-> d, a&b&c&d
|
||||
{a && b && c[+]} <>-> d, a&b&c&d
|
||||
{a && b && c[=1]} <>-> d, a&b&c&d
|
||||
{a && b && d[=2]} <>-> d, 0
|
||||
{a && b && d[*2..]} <>-> d, 0
|
||||
{a && b && d[->2..4]} <>-> d, 0
|
||||
{a && { c* : b* : (g|h)*}} <>-> d, a & c & b & (g | h) & d
|
||||
{a && {b;c}} <>-> d, 0
|
||||
{a && {(b;c):e}} <>-> d, 0
|
||||
# until better
|
||||
{a && {b*;c*}} <>-> d, {a && {b*|c*}} <>-> d
|
||||
# until better
|
||||
{a && {(b*;c*):e}} <>-> d, {a && {b*|c*} && e} <>-> d
|
||||
{a && {b*;c}} <>-> d, a & c & d
|
||||
{a && {(b*;c):e}} <>-> d, a & c & d & e
|
||||
{a && {b;c*}} <>-> d, a & b & d
|
||||
{a && {(b;c*):e}} <>-> d, a & b & d & e
|
||||
{{{b1;r1*}&&{b2;r2*}};c}, b1&b2&X{{r1*&&r2*};c}
|
||||
{{b1:r1*}&&{b2:r2*}}, {{b1&&b2}:{r1*&&r2*}}
|
||||
{{r1*;b1}&&{r2*;b2}}, {{r1*&&r2*};{b1&&b2}}
|
||||
{{r1*:b1}&&{r2*:b2}}, {{r1*&&r2*}:{b1&&b2}}
|
||||
{{a;b*;c}&&{d;e*}&&{f*;g}&&{h*}}, {{f*;g}&&{h*}&&{{a&&d};{e* && {b*;c}}}}
|
||||
{{{b1;r1*}&{b2;r2*}};c}, b1&b2&X{{r1*&r2*};c}
|
||||
{{b1:(r1;x1*)}&{b2:(r2;x2*)}}, {{b1&&b2}:{{r1&&r2};{x1*&x2*}}}
|
||||
# Not reduced
|
||||
{{b1:r1*}&{b2:r2*}}, {{b1:r1*}&{b2:r2*}}
|
||||
# Not reduced
|
||||
{{r1*;b1}&{r2*;b2}}, {{r1*;b1}&{r2*;b2}}
|
||||
# Not reduced
|
||||
{{r1*:b1}&{r2*:b2}}, {{r1*:b1}&{r2*:b2}}
|
||||
{{a;b*;c}&{d;e*}&{f*;g}&{h*}}, {{f*;g}&{h*}&{{a&&d};{e* & {b*;c}}}}
|
||||
{a;(b*;c*;([*0]+{d;e}))*}!, {a;{b|c|{d;e}}*}!
|
||||
{a&b&c*}|->!Xb, (X!b | !(a & b)) & (!(a & b) | !c | X(!c R !b))
|
||||
{[*]}[]->b, Gb
|
||||
{a;[*]}[]->b, Gb | !a
|
||||
{[*];a}[]->b, G(b | !a)
|
||||
{a;b;[*]}[]->c, !a | X(!b | Gc)
|
||||
{a;a;[*]}[]->c, !a | X(!a | Gc)
|
||||
{s[*]}[]->b, b W !s
|
||||
{s[+]}[]->b, b W !s
|
||||
{s[*2..]}[]->b, !s | X(b W !s)
|
||||
{a;b*;c;d*}[]->e, !a | X(!b R ((e & X(e W !d)) | !c))
|
||||
{a:b*:c:d*}[]->e, !a | ((!c | (e W !d)) W !b)
|
||||
{a|b*|c|d*}[]->e, (e | !(a | c)) & (e W !b) & (e W !d)
|
||||
{{[*0]|a};b;{[*0]|a};c;e[*]}[]->f,{{[*0]|a};b;{[*0]|a}}[]->X((f&X(f W !e))|!c)
|
||||
|
||||
# not reduced
|
||||
run 0 $x '{a;(b[*2..4];c*;([*0]+{d;e}))*}!' \
|
||||
'{a;(b[*2..4];c*;([*0]+{d;e}))*}!'
|
||||
run 0 $x '{((a*;b)+[*0])[*4..6]}!' '{((a*;b))[*0..6]}!'
|
||||
run 0 $x '{c[*];e[*]}[]-> a' '{c[*];e[*]}[]-> a'
|
||||
;;
|
||||
esac
|
||||
{a&b&c*}<>->!Xb, (a & b & X!b) | (a & b & c & X(c U !b))
|
||||
{[*]}<>->b, Fb
|
||||
{a;[*]}<>->b, Fb & a
|
||||
{[*];a}<>->b, F(a & b)
|
||||
{a;b;[*]}<>->c, a & X(b & Fc)
|
||||
{a;a;[*]}<>->c, a & X(a & Fc)
|
||||
{s[*]}<>->b, b M s
|
||||
{s[+]}<>->b, b M s
|
||||
{s[*2..]}<>->b, s & X(b M s)
|
||||
{1:a*}!, a
|
||||
{(1;1):a*}!, Xa
|
||||
{a;b*;c;d*}<>->e, a & X(b U (c & (e | X(e M d))))
|
||||
{a:b*:c:d*}<>->e, a & ((c & (e M d)) M b)
|
||||
{a|b*|c|d*}<>->e, ((a | c) & e) | (e M b) | (e M d)
|
||||
{{[*0]|a};b;{[*0]|a};c;e[*]}<>->f, {{[*0]|a};b;{[*0]|a}}<>->X(c&(f|X(f M e)))
|
||||
{a;b[*];c[*];e;f*}, a & X(b W (c W e))
|
||||
{a;b*;(a* && (b;c));c*}, a & X(b W {a[*] && {b;c}})
|
||||
{a;a;b[*2..];b}, a & X(a & X(b & X(b & Xb)))
|
||||
!{a;a;b[*2..];b}, !a | X(!a | X(!b | X(!b | X!b)))
|
||||
!{a;b[*];c[*];e;f*}, !a | X(!b M (!c M !e))
|
||||
!{a;b*;(a* && (b;c));c*}, !a | X(!b M !{a[*] && {b;c}})
|
||||
{(a;c*;d)|(b;c)}, (a & X(c W d)) | (b & Xc)
|
||||
!{(a;c*;d)|(b;c)}, (X(!c M !d) | !a) & (X!c | !b)
|
||||
(Xc R b) & (Xc W 0), b & XGc
|
||||
{{c*|1}[*0..1]}<>-> v, {{c[+]|1}[*0..1]}<>-> v
|
||||
{{b*;c*}[*3..5]}<>-> v, {{b*;c*}[*0..5]} <>-> v
|
||||
{{b*&c*}[*3..5]}<>-> v, {{b[+]|c[+]}[*0..5]} <>-> v
|
||||
# not reduced
|
||||
{a;(b[*2..4];c*;([*0]+{d;e}))*}!, {a;(b[*2..4];c*;([*0]+{d;e}))*}!
|
||||
{((a*;b)+[*0])[*4..6]}!, {((a*;b))[*0..6]}!
|
||||
{c[*];e[*]}[]-> a, {c[*];e[*]}[]-> a
|
||||
EOF
|
||||
|
||||
run 0 $x 'a R (b W G(c))' 'a R (b W G(c))' #not reduced
|
||||
|
||||
run 0 $x 'a M ((a&b) R c)' 'a M ((a&b) R c)' #not reduced.
|
||||
run 0 $x '(a&b) W (a U c)' '(a&b) W (a U c)' #not reduced.
|
||||
|
||||
# Eventuality and universality class reductions
|
||||
run 0 $x 'FFa' 'Fa'
|
||||
run 0 $x 'FGFa' 'GFa'
|
||||
run 0 $x 'b U Fa' 'Fa'
|
||||
run 0 $x 'b U GFa' 'GFa'
|
||||
run 0 $x 'Ga' 'Ga'
|
||||
|
||||
run 0 $x 'a U XXXFb' 'XXXFb'
|
||||
done
|
||||
run 0 ../reduccmp nottau.txt
|
||||
run 0 ../reductaustr common.txt
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
#! /bin/sh
|
||||
# Copyright (C) 2012 Laboratoire de Recherche et Developpement
|
||||
# Copyright (C) 2012, 2014 Laboratoire de Recherche et Developpement
|
||||
# de l'Epita (LRDE).
|
||||
#
|
||||
# This file is part of Spot, a model checking library.
|
||||
|
|
@ -22,52 +22,39 @@
|
|||
# These formulas comes from an appendix of tl/tl.tex
|
||||
|
||||
. ./defs || exit 1
|
||||
|
||||
set -e
|
||||
|
||||
equiv()
|
||||
{
|
||||
dst=$1
|
||||
shift
|
||||
for src in "$@"; do
|
||||
../reduccmp "$src" "$dst"
|
||||
done
|
||||
}
|
||||
|
||||
cat >input.txt<<EOF
|
||||
# Equivalences with U
|
||||
|
||||
equiv Ff '1 U f'
|
||||
equiv Gf '!F!f' '!(1 U!f)'
|
||||
equiv 'f W g' '(f U g) | (G f)' '(f U g) | !(1 U ! f)' \
|
||||
'f U (g | G f)' 'f U (g | !(1 U ! f ))'
|
||||
equiv 'f M g' 'g U (f & g)'
|
||||
equiv 'f R g' 'g W (f & g)' '(g U (f & g)) | !(1 U ! g)' \
|
||||
'g U ((f & g) | !(1 U ! g))'
|
||||
1 U f, Ff
|
||||
!F!f, !(1 U!f), Gf
|
||||
(f U g)|(G f), (f U g) | !(1 U ! f), f U (g | G f), f U (g | !(1 U !f)), f W g
|
||||
g U (f & g), f M g
|
||||
g W (f & g), (g U (f & g)) | !(1 U ! g), g U ((f & g) | !(1 U ! g)), f R g
|
||||
|
||||
# Equivalences with W
|
||||
|
||||
equiv Ff '!G!f' '!((! f) W 0)'
|
||||
equiv Gf '0 R f' 'f W 0'
|
||||
equiv 'f U g' '(f W g) & (F g)' '(f W g) & !((! g) W 0)'
|
||||
equiv 'f M g' '(g W (f & g)) & (F f)' '(g W (f & g)) & !((!f) W 0)'
|
||||
equiv 'f R g' 'g W (f & g)'
|
||||
!G!f, !((! f) W 0), Ff
|
||||
0 R f, f W 0, Gf
|
||||
(f W g) & (F g), (f W g) & !((! g) W 0), f U g
|
||||
(g W (f & g)) & (F f), (g W (f & g)) & !((!f) W 0), f M g
|
||||
g W (f & g), f R g
|
||||
|
||||
# Equivalences with R
|
||||
!G!f, !(0 R !f), Ff
|
||||
0 R f, Gf
|
||||
# (((X g) R f) & F g) | g, (((X g) R f ) & (!(0 R ! g))) | g, f U g
|
||||
((X g) R f) | g, g R (f | g), f W g
|
||||
(f R g) & F f, (f R g) & !(0 R !f), f R (g & F f), f R (g & !(0 R !f)), f M g
|
||||
|
||||
equiv Ff '!G!f' '!(0 R !f)'
|
||||
equiv Gf '0 R f'
|
||||
#equiv 'f U g' '(((X g) R f) & F g) | g' '(((X g) R f ) & (!(0 R ! g))) | g'
|
||||
equiv 'f W g' '((X g) R f) | g' 'g R (f | g)'
|
||||
equiv 'f M g' '( f R g) & F f' '(f R g) & ! (0 R ! f)' \
|
||||
'f R (g & F f)' 'f R (g & !(0 R !f))'
|
||||
# Equivalences with M
|
||||
|
||||
equiv Ff 'f M 1'
|
||||
equiv Gf '!F!f' '!((!f) M 1)'
|
||||
equiv 'f U g' '((X g) M f) | g' 'g M (f | g)'
|
||||
equiv 'f W g' '(f U g) | G f' '((X g) M f) | g | !((! f ) M 1)'
|
||||
equiv 'f R g' '(f M g) | G g' '(f M g) | !((! g) M 1)'
|
||||
f M 1, Ff
|
||||
!F!f, !((!f) M 1), Gf
|
||||
((X g) M f) | g, g M (f | g), f U g
|
||||
(f U g) | G f, ((X g) M f) | g | !((! f ) M 1), f W g
|
||||
(f M g) | G g, (f M g) | !((! g) M 1), f R g
|
||||
|
||||
# Example from tl.tex
|
||||
#(((f U (Xg & f))|!(1 U !f))&(1 U Xg)) | g, f U g
|
||||
EOF
|
||||
|
||||
# equiv 'f U g' '(((f U (Xg & f))|!(1 U !f))&(1 U Xg)) | g'
|
||||
run 0 ../reduccmp input.txt
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue