alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
spot/iface/gspn/ltlgspn.cc
Alexandre Duret-Lutz e3de75f677 * src/tgbaalgos/projrun.hh, src/tgbaalgos/projrun.cc: New files. 
* src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS,
libtgbaalgos_la_SOURCES): Add them.
* iface/gspn/ltlgspn.cc (main): Call project_tgba_run if -P.
2004-11-02 16:26:57 +00:00

351 lines
8.5 KiB
C++
Raw Blame History

// 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.
//
// 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 SSP
#include "gspn.hh"
#define MIN_ARG 3
#else
#include "ssp.hh"
#define MIN_ARG 4
#include "tgba/tgbaexplicit.hh"
#include "tgbaparse/public.hh"
#endif
#include "ltlparse/public.hh"
#include "ltlvisit/destroy.hh"
#include "tgba/tgbatba.hh"
#include "tgba/tgbaproduct.hh"
#include "tgbaalgos/ltl2tgba_lacim.hh"
#include "tgbaalgos/ltl2tgba_fm.hh"
#include "tgbaalgos/magic.hh"
#include "tgbaalgos/gtec/gtec.hh"
#include "tgbaalgos/gtec/ce.hh"
#include "tgbaalgos/projrun.hh"
void
syntax(char* prog)
{
std::cerr << "Usage: "<< prog
#ifndef SSP
<< " [OPTIONS...] model formula props..." << std::endl
#else
<< " [OPTIONS...] model formula automata props..." << std::endl
#endif
<< std::endl
<< " -c compute an example" << std::endl
<< " (instead of just checking for emptiness)" << std::endl
<< std::endl
#ifndef SSP
<< " -d DEAD" << std::endl
<< " use DEAD as property for marking dead states"
<< " (by default DEAD=true)" << std::endl
#endif
<< " -e use Couvreur's emptiness-check (default)" << std::endl
<< " -e2 use Couvreur's emptiness-check's shy variant" << std::endl
#ifdef SSP
<< " -e3 use semi-d. incl. Couvreur's emptiness-check"
<< std::endl
<< " -e4 use semi-d. incl. Couvreur's emptiness-check's "
<< "shy variant"
<< std::endl
<< " -e5 use d. incl. Couvreur's emptiness-check's shy variant"
<< std::endl
#endif
<< " -m degeneralize and perform a magic-search" << std::endl
<< std::endl
<< " -l use Couvreur's LaCIM algorithm for translation (default)"
<< std::endl
<< " -f use Couvreur's FM algorithm for translation" << std::endl
<< " -P do not project example on model" << std::endl;
exit(2);
}
int
main(int argc, char **argv)
try
{
int formula_index = 1;
enum { Couvreur, Couvreur2, Couvreur3,
Couvreur4, Couvreur5, Magic } check = Couvreur;
enum { Lacim, Fm } trans = Lacim;
bool compute_counter_example = false;
bool proj = true;
std::string dead = "true";
spot::ltl::declarative_environment env;
while (formula_index < argc && *argv[formula_index] == '-')
{
if (!strcmp(argv[formula_index], "-c"))
{
compute_counter_example = true;
}
#ifndef SSP
else if (!strcmp(argv[formula_index], "-d"))
{
if (formula_index + 1 >= argc)
syntax(argv[0]);
dead = argv[++formula_index];
if (strcasecmp(dead.c_str(), "true")
&& strcasecmp(dead.c_str(), "false"))
env.declare(dead);
}
#endif
else if (!strcmp(argv[formula_index], "-e"))
{
check = Couvreur;
}
else if (!strcmp(argv[formula_index], "-e2"))
{
check = Couvreur2;
}
#ifdef SSP
else if (!strcmp(argv[formula_index], "-e3"))
{
check = Couvreur3;
}
else if (!strcmp(argv[formula_index], "-e4"))
{
check = Couvreur4;
}
else if (!strcmp(argv[formula_index], "-e5"))
{
check = Couvreur5;
}
#endif
else if (!strcmp(argv[formula_index], "-m"))
{
check = Magic;
}
else if (!strcmp(argv[formula_index], "-l"))
{
trans = Lacim;
}
else if (!strcmp(argv[formula_index], "-f"))
{
trans = Fm;
}
else if (!strcmp(argv[formula_index], "-P"))
{
proj = 0;
}
else
{
syntax(argv[0]);
}
++formula_index;
}
if (argc < formula_index + MIN_ARG)
syntax(argv[0]);
while (argc >= formula_index + MIN_ARG)
{
env.declare(argv[argc - 1]);
--argc;
}
spot::ltl::parse_error_list pel;
spot::ltl::formula* f = spot::ltl::parse(argv[formula_index + 1],
pel, env);
if (spot::ltl::format_parse_errors(std::cerr,
argv[formula_index + 1], pel))
exit(2);
argv[1] = argv[formula_index];
spot::bdd_dict* dict = new spot::bdd_dict();
#if SSP
bool inclusion = (check != Couvreur && check != Couvreur2);
spot::gspn_ssp_interface gspn(2, argv, dict, env, inclusion);
spot::tgba_parse_error_list pel1;
spot::tgba_explicit* control = spot::tgba_parse(argv[formula_index + 2],
pel1, dict, env);
if (spot::format_tgba_parse_errors(std::cerr, pel1))
return 2;
#else
spot::gspn_interface gspn(2, argv, dict, env, dead);
#endif
spot::tgba* a_f = 0;
switch (trans)
{
case Fm:
a_f = spot::ltl_to_tgba_fm(f, dict);
break;
case Lacim:
a_f = spot::ltl_to_tgba_lacim(f, dict);
break;
}
spot::ltl::destroy(f);
#ifndef SSP
spot::tgba* model = gspn.automaton();
spot::tgba_product* prod = new spot::tgba_product(model, a_f);
#else
spot::tgba_product* ca = new spot::tgba_product(control, a_f);
spot::tgba* model = gspn.automaton(ca);
spot::tgba* prod = model;
#endif
switch (check)
{
case Couvreur:
case Couvreur2:
case Couvreur3:
case Couvreur4:
case Couvreur5:
{
spot::couvreur99_check* ec;
switch (check)
{
case Couvreur:
ec = new spot::couvreur99_check(prod);
break;
case Couvreur2:
ec = new spot::couvreur99_check_shy(prod);
break;
#ifdef SSP
case Couvreur3:
ec = spot::couvreur99_check_ssp_semi(prod);
break;
case Couvreur4:
ec = spot::couvreur99_check_ssp_shy_semi(prod);
break;
case Couvreur5:
ec = spot::couvreur99_check_ssp_shy(prod);
break;
#endif
default:
assert(0);
// Assign something so that GCC does not complains
// EC might be used uninitialized if assert is disabled.
ec = 0;
}
spot::emptiness_check_result* res = ec->check();
const spot::couvreur99_check_status* ecs = ec->result();
if (res)
{
if (compute_counter_example)
{
spot::couvreur99_check_result* ce;
#ifndef SSP
ce = new spot::couvreur99_check_result(ecs);
#else
switch (check)
{
case Couvreur:
case Couvreur2:
case Couvreur5:
ce = new spot::couvreur99_check_result(ecs);
break;
default:
ce = spot::counter_example_ssp(ecs);
}
#endif
spot::tgba_run* run = ce->accepting_run();
if (proj)
{
spot::tgba_run* p = project_tgba_run(prod, model, run);
spot::print_tgba_run(std::cout, model, p);
delete p;
}
else
{
spot::print_tgba_run(std::cout, prod, run);
}
ce->print_stats(std::cout);
delete run;
delete ce;
}
else
{
std::cout << "non empty" << std::endl;
ecs->print_stats(std::cout);
}
delete res;
}
else
{
std::cout << "empty" << std::endl;
ecs->print_stats(std::cout);
}
std::cout << std::endl;
delete ec;
if (res)
exit(1);
}
break;
case Magic:
{
spot::tgba_tba_proxy* d = new spot::tgba_tba_proxy(prod);
spot::magic_search ms(d);
spot::emptiness_check_result* res = ms.check();
if (res)
{
if (compute_counter_example)
{
spot::tgba_run* run = res->accepting_run();
if (proj)
{
spot::tgba_run* p = project_tgba_run(prod, model, run);
spot::print_tgba_run(std::cout, model, p);
delete p;
}
else
{
spot::print_tgba_run(std::cout, prod, run);
}
delete run;
}
else
std::cout << "non-empty" << std::endl;
delete res;
exit(1);
}
else
{
std::cout << "empty" << std::endl;
}
delete d;
}
}
#ifndef SSP
delete prod;
delete model;
#else
delete model;
delete control;
#endif
delete a_f;
delete dict;
}
catch (spot::gspn_exeption e)
{
std::cerr << e << std::endl;
throw;
}
Reference in a new issue View git blame Copy permalink