Commit 830e4828 authored by Damien Lefortier's avatar Damien Lefortier
Browse files

Merge eltl2tgba.cc into ltl2tgba.cc.

* src/tgbatest/eltl2tgba.cc: Remove.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbatest/ltl2tgba.cc: New option: -xltl to translate an
extended LTL instead of an LTL, a feature previously offered by
eltl2tgba.cc. Also: -R3b to use delete_unaccepting_scc.
* src/tgbatest/spotlbtt.test: Adjust.
parent 1aa10e13
2010-01-05 Damien Lefortier <dam@lrde.epita.fr>
Merge eltl2tgba.cc into ltl2tgba.cc.
* src/tgbatest/eltl2tgba.cc: Remove.
* src/tgbatest/Makefile.am: Adjust.
* src/tgbatest/ltl2tgba.cc: New option: -xltl to translate an
extended LTL instead of an LTL, a feature previously offered by
eltl2tgba.cc. Also: -R3b to use delete_unaccepting_scc.
* src/tgbatest/spotlbtt.test: Adjust.
2009-11-10 Damien Lefortier <dam@lrde.epita.fr>
* src/tgba/tgbabddcoredata.cc (delete_unaccepting_scc): Fix a bug.
......
......@@ -25,7 +25,7 @@ LDADD = ../libspot.la
# These are the most used test programs, and they are also useful
# to run manually outside the test suite. Always build them.
noinst_PROGRAMS = eltl2tgba ltl2tgba randtgba
noinst_PROGRAMS = ltl2tgba randtgba
check_SCRIPTS = defs
# Keep this sorted alphabetically.
......@@ -49,7 +49,6 @@ check_PROGRAMS = \
bddprod_SOURCES = ltlprod.cc
bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT
complement_SOURCES = complementation.cc
eltl2tgba_SOURCES = eltl2tgba.cc
explicit_SOURCES = explicit.cc
expldot_SOURCES = powerset.cc
expldot_CXXFLAGS = -DDOTTY
......
// Copyright (C) 2008, 2009 Laboratoire de Recherche et Developpement
// 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 <sstream>
#include <fstream>
#include <cassert>
#include <cstring>
#include "ltlparse/public.hh"
#include "eltlparse/public.hh"
#include "tgbaalgos/eltl2tgba_lacim.hh"
#include "tgbaalgos/dotty.hh"
#include "tgbaalgos/lbtt.hh"
#include "tgbaalgos/save.hh"
#include "ltlvisit/tostring.hh"
#include "ltlast/allnodes.hh"
void
syntax(char* prog)
{
std::cerr << "Usage: " << prog << " [OPTIONS...] formula [file]" << std::endl
<< " " << prog << " -F [OPTIONS...] file [file]" << std::endl
<< " " << prog << " -L [OPTIONS...] file [file]" << std::endl
<< " " << prog << " -LW [OPTIONS...] file [file]" << std::endl
<< std::endl
<< "Options:" << std::endl
<< " -F read the formula from the file (extended input format)"
<< std::endl
<< " -L read the formula from an LBTT-compatible file"
<< std::endl
<< " -LW read the formula from an LBTT-compatible file"
<< " (with no reduction)"
<< std::endl;
}
std::string
ltl_defs()
{
std::string s = "\
X=(0 1 true \
1 2 $0 \
accept 2) \
U=(0 0 $0 \
0 1 $1 \
accept 1) \
G=(0 0 $0) \
F=U(true, $0) \
R=!U(!$0, !$1)";
return s;
}
int
main(int argc, char** argv)
{
if (argc < 2)
{
syntax(argv[0]);
return 1;
}
spot::eltl::parse_error_list p;
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::ltl::formula* f = 0;
int formula_index = 0;
int reduce = 1;
if (strcmp(argv[1], "-F") == 0)
{
f = spot::eltl::parse_file(argv[2], p, env, false);
formula_index = 2;
}
if (strcmp(argv[1], "-L") == 0 || strcmp(argv[1], "-LW") == 0)
{
reduce = strcmp(argv[1], "-LW") == 0 ? 0 : 1;
std::string input;
std::ifstream ifs(argv[2]);
std::getline(ifs, input, '\0');
spot::ltl::parse_error_list p_;
f = spot::ltl::parse(input, p_, env, false);
input = ltl_defs();
input += "%";
input += spot::ltl::to_string(f, true);
f->destroy();
f = spot::eltl::parse_string(input, p, env, false);
formula_index = 2;
}
if (formula_index == 0)
{
std::stringstream oss;
oss << ltl_defs() << "%" << argv[1];
f = spot::eltl::parse_string(oss.str(), p, env, false);
formula_index = 1;
}
if (spot::eltl::format_parse_errors(std::cerr, p))
{
if (f != 0)
std::cout << f->dump() << std::endl;
return 1;
}
assert(f != 0);
std::cerr << f->dump() << std::endl;
spot::bdd_dict* dict = new spot::bdd_dict();
spot::tgba_bdd_concrete* concrete = spot::eltl_to_tgba_lacim(f, dict);
if (reduce == 1)
concrete->delete_unaccepting_scc();
if (strcmp(argv[1], "-L") == 0 || strcmp(argv[1], "-LW") == 0)
spot::lbtt_reachable(std::cout, concrete);
else
{
spot::dotty_reachable(std::cout, concrete);
if (formula_index + 1 < argc)
{
std::ofstream ofs(argv[formula_index + 1]);
spot::tgba_save_reachable(ofs, concrete);
ofs.close();
}
}
f->destroy();
delete concrete;
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);
assert(spot::ltl::automatop::instance_count() == 0);
delete dict;
}
......@@ -6,7 +6,7 @@ set -e
# Check if the TGBA was corretly constructed.
check_construct()
{
run 0 ../eltl2tgba -F "$1" input
run 0 ../ltl2tgba -F -l -xltl -b "$1" > output
}
# Check if the TGBA behaves correctly by doing an emptiness check on
......@@ -14,11 +14,11 @@ check_construct()
# translated using FM.
check_true()
{
run 0 ../ltl2tgba -e -Pinput -f "$1"
run 0 ../ltl2tgba -e -Poutput -f "$1"
}
check_false()
{
run 1 ../ltl2tgba -e -Pinput -f "$1"
run 1 ../ltl2tgba -e -Poutput -f "$1"
}
# Create the prelude file.
......
......@@ -49,12 +49,30 @@
#include "tgbaalgos/replayrun.hh"
#include "tgbaalgos/rundotdec.hh"
#include "tgbaalgos/sccfilter.hh"
#include "tgbaalgos/eltl2tgba_lacim.hh"
#include "eltlparse/public.hh"
#include "misc/timer.hh"
#include "tgbaalgos/stats.hh"
#include "tgbaalgos/scc.hh"
#include "tgbaalgos/emptiness_stats.hh"
std::string
ltl_defs()
{
std::string s = "\
X=(0 1 true \
1 2 $0 \
accept 2) \
U=(0 0 $0 \
0 1 $1 \
accept 1) \
G=(0 0 $0) \
F=U(true, $0) \
R=!U(!$0, !$1)";
return s;
}
void
syntax(char* prog)
{
......@@ -125,6 +143,7 @@ syntax(char* prog)
<< "reachability graph"
<< std::endl
<< " -A same as -a, but as a set" << std::endl
<< " -xltl translate an extended LTL, not an LTL" << std::endl
<< " -r display the relation BDD, not the reachability graph"
<< std::endl
<< " -R same as -r, but as a set" << std::endl
......@@ -170,6 +189,7 @@ syntax(char* prog)
<< " -R2t remove transitions using delayed simulation"
<< std::endl
<< " -R3 use SCC to reduce the automata" << std::endl
<< " -R3b delete unaccepting SCC directly on the BDD" << std::endl
<< " -Rd display the simulation relation" << std::endl
<< " -RD display the parity game (dot format)" << std::endl
<< std::endl
......@@ -254,6 +274,8 @@ main(int argc, char** argv)
bool from_file = false;
int reduc_aut = spot::Reduce_None;
int redopt = spot::ltl::Reduce_None;
bool eltl = false;
bool delete_unaccepting_scc = false;
bool display_reduce_form = false;
bool display_rel_sim = false;
bool display_parity_game = false;
......@@ -351,6 +373,10 @@ main(int argc, char** argv)
expect_counter_example = false;
output = -1;
}
else if (!strcmp(argv[formula_index], "-xltl"))
{
eltl = true;
}
else if (!strcmp(argv[formula_index], "-taa"))
{
translation = TransTAA;
......@@ -528,6 +554,10 @@ main(int argc, char** argv)
{
reduc_aut |= spot::Reduce_Scc;
}
else if (!strcmp(argv[formula_index], "-R3b"))
{
delete_unaccepting_scc = true;
}
else if (!strcmp(argv[formula_index], "-rd"))
{
display_reduce_form = true;
......@@ -634,11 +664,40 @@ main(int argc, char** argv)
spot::ltl::formula* f = 0;
if (!from_file)
{
spot::ltl::parse_error_list pel;
tm.start("parsing formula");
f = spot::ltl::parse(input, pel, env, debug_opt);
tm.stop("parsing formula");
exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel);
if (!eltl)
{
spot::ltl::parse_error_list pel;
tm.start("parsing formula");
f = spot::ltl::parse(input, pel, env, debug_opt);
tm.stop("parsing formula");
exit_code = spot::ltl::format_parse_errors(std::cerr, input, pel);
}
else if (!file_opt || output == 6)
{
// Call the LTL parser first to handle abbreviations such as
// [] when the formula is not given in a file or when the
// output in done in LBTT's format. The ELTL parser is then
// called with usual LTL operators.
spot::ltl::parse_error_list pel;
tm.start("parsing formula");
f = spot::ltl::parse(input, pel, env, debug_opt);
input = ltl_defs();
input += "%";
input += spot::ltl::to_string(f, true);
f->destroy();
spot::eltl::parse_error_list p;
f = spot::eltl::parse_string(input, p, env, debug_opt);
tm.stop("parsing formula");
exit_code = spot::eltl::format_parse_errors(std::cerr, p);
}
else
{
spot::eltl::parse_error_list p;
tm.start("parsing formula");
f = spot::eltl::parse_string(input, p, env, false);
tm.stop("parsing formula");
exit_code = spot::eltl::format_parse_errors(std::cerr, p);
}
}
if (f || from_file)
{
......@@ -690,7 +749,10 @@ main(int argc, char** argv)
a = spot::ltl_to_taa(f, dict, containment);
break;
case TransLaCIM:
a = concrete = spot::ltl_to_tgba_lacim(f, dict);
if (!eltl)
a = concrete = spot::ltl_to_tgba_lacim(f, dict);
else
a = concrete = spot::eltl_to_tgba_lacim(f, dict);
break;
}
tm.stop("translating formula");
......@@ -727,6 +789,15 @@ main(int argc, char** argv)
tm.stop("reducing A_f w/ SCC");
}
if (delete_unaccepting_scc)
{
tm.start("reducing A_f w/ SCC on BDD");
if (spot::tgba_bdd_concrete* bc =
dynamic_cast<spot::tgba_bdd_concrete*>(a))
bc->delete_unaccepting_scc();
tm.stop("reducing A_f w/ SCC on BDD");
}
if (reduc_aut & ~spot::Reduce_Scc)
{
tm.start("reducing A_f w/ sim.");
......
......@@ -32,7 +32,7 @@ Algorithm
{
Name = "Spot (Couvreur -- LaCIM)"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -F -l -t'"
Parameters = "--spot '../ltl2tgba -l -F -t'"
Enabled = yes
}
......@@ -40,7 +40,7 @@ Algorithm
{
Name = "Spot (Couvreur -- LaCIM), reduction of formula"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -r4 -l -F -t'"
Parameters = "--spot '../ltl2tgba -l -F -t -r4'"
Enabled = yes
}
......@@ -49,7 +49,7 @@ Algorithm
Name = "Spot (Couvreur -- LaCIM), degeneralized"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -l -F -t -D'"
Enabled = yes
Enabled = no
}
Algorithm
......@@ -64,7 +64,7 @@ Algorithm
{
Name = "Spot (Couvreur -- LaCIM), eltl"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../eltl2tgba -LW'"
Parameters = "--spot '../ltl2tgba -F -l -t -xltl'"
Enabled = yes
}
......@@ -72,10 +72,18 @@ Algorithm
{
Name = "Spot (Couvreur -- LaCIM), eltl + delete_unaccepting_scc"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../eltl2tgba -L'"
Parameters = "--spot '../ltl2tgba -F -l -t -xltl -R3b'"
Enabled = yes
}
Algorithm
{
Name = "Spot (Couvreur -- LaCIM), eltl + post reduction with scc"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -F -l -t -xltl -R3'"
Enabled = no
}
Algorithm
{
Name = "Spot (Couvreur -- FM)"
......@@ -276,12 +284,20 @@ Algorithm
Enabled = yes
}
Algorithm
{
Name = "Spot (Tauriainen -- TAA), refined rules + post reduction with scc"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -F -taa -t -c -R3'"
Enabled = yes
}
Algorithm
{
Name = "Spot (Tauriainen -- TAA) refined rules + pre + post reduction"
Path = "${LBTT_TRANSLATE}"
Parameters = "--spot '../ltl2tgba -F -taa -t -c -r7 -R3'"
Enabled = yes
Enabled = no
}
GlobalOptions
......
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