Commit fd12c023 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz

* src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product):

New constructor.
* src/tgba/tgbaproduct.hh (state_bdd_product::state_bdd_product):
New constructor.
* tgbatest/tripprod.cc, tgbatest/tripprod.test: New files.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
(tripprod_SOURCES): New variable.
(CLEANFILES): Add input3.
(TESTS): Add tripprod.test.
parent 4db70160
2003-06-17 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgbaproduct.cc (state_bdd_product::state_bdd_product):
New constructor.
* src/tgba/tgbaproduct.hh (state_bdd_product::state_bdd_product):
New constructor.
* tgbatest/tripprod.cc, tgbatest/tripprod.test: New files.
* src/tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
(tripprod_SOURCES): New variable.
(CLEANFILES): Add input3.
(TESTS): Add tripprod.test.
2003-06-16 Alexandre Duret-Lutz <aduret@src.lip6.fr>
* src/tgba/tgbabddprod.cc, src/tgba/tgbabddprod.hh: Rename as ...
......@@ -46,6 +58,7 @@
* tgba/tgbaexplicit.cc (state_explicit::clone): New method.
* src/tgba/tgbaexplicit.cc (tgba_explicit::get_condition,
tgba_explicit::get_promise): Call ltl::destroy on existing formulae.
* tgbatest/explprod.cc, tgbatest/explprod.test: New files.
* tgbatest/Makefile.am (check_PROGRAMS): Add explprod.
(explprod_SOURCES): New variable.
(TESTS): Add explprod.test.
......
......@@ -9,6 +9,13 @@ namespace spot
////////////////////////////////////////////////////////////
// state_bdd_product
state_bdd_product::state_bdd_product(const state_bdd_product& o)
: state_bdd(o.as_bdd()),
left_(o.left()->clone()),
right_(o.right()->clone())
{
}
state_bdd_product::~state_bdd_product()
{
delete left_;
......
......@@ -26,6 +26,9 @@ namespace spot
{
}
/// Copy constructor
state_bdd_product(const state_bdd_product& o);
virtual ~state_bdd_product();
state*
......
......@@ -12,3 +12,4 @@ bddprod
explprod
*.ps
*.dot
tripprod
......@@ -10,16 +10,18 @@ check_PROGRAMS = \
ltl2tgba \
ltlprod \
bddprod \
explprod
explprod \
tripprod
bddprod_SOURCES = ltlprod.cc
bddprod_SOURCES = ltlprod.cc
bddprod_CXXFLAGS = -DBDD_CONCRETE_PRODUCT
explicit_SOURCES = explicit.cc
explprod_SOURCES = explprod.cc
ltl2tgba_SOURCES = ltl2tgba.cc
ltlprod_SOURCES = ltlprod.cc
ltlprod_SOURCES = ltlprod.cc
readsave_SOURCES = readsave.cc
tgbaread_SOURCES = tgbaread.cc
tripprod_SOURCES = tripprod.cc
TESTS = \
explicit.test \
......@@ -28,8 +30,9 @@ TESTS = \
ltl2tgba.test \
ltlprod.test \
bddprod.test \
explprod.test
explprod.test \
tripprod.test
EXTRA_DIST = $(TESTS)
CLEANFILES = input input1 input2 stdout expected
CLEANFILES = input input1 input2 input3 stdout expected
......@@ -29,9 +29,9 @@ main(int argc, char** argv)
return 2;
spot::tgba_parse_error_list pel2;
spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, env);
if (spot::format_tgba_parse_errors(std::cerr, pel1))
if (spot::format_tgba_parse_errors(std::cerr, pel2))
return 2;
{
spot::tgba_product p(*a1, *a2);
spot::tgba_save_reachable(std::cout, p);
......
#include <iostream>
#include <cassert>
#include "tgba/ltl2tgba.hh"
#include "tgba/tgbaexplicit.hh"
#include "tgba/tgbaproduct.hh"
#include "tgbaparse/public.hh"
#include "tgbaalgos/save.hh"
#include "ltlast/allnodes.hh"
void
syntax(char* prog)
{
std::cerr << prog << " file1 file2 file3" << std::endl;
exit(2);
}
int
main(int argc, char** argv)
{
int exit_code = 0;
if (argc != 4)
syntax(argv[0]);
spot::ltl::environment& env(spot::ltl::default_environment::instance());
spot::tgba_parse_error_list pel1;
spot::tgba_explicit* a1 = spot::tgba_parse(argv[1], pel1, env);
if (spot::format_tgba_parse_errors(std::cerr, pel1))
return 2;
spot::tgba_parse_error_list pel2;
spot::tgba_explicit* a2 = spot::tgba_parse(argv[2], pel2, env);
if (spot::format_tgba_parse_errors(std::cerr, pel2))
return 2;
spot::tgba_parse_error_list pel3;
spot::tgba_explicit* a3 = spot::tgba_parse(argv[3], pel3, env);
if (spot::format_tgba_parse_errors(std::cerr, pel3))
return 2;
{
spot::tgba_product p(*a1, *a2);
spot::tgba_product p2(p, *a3);
spot::tgba_save_reachable(std::cout, p2);
}
assert(spot::ltl::unop::instance_count() == 0);
assert(spot::ltl::binop::instance_count() == 0);
assert(spot::ltl::multop::instance_count() == 0);
assert(spot::ltl::atomic_prop::instance_count() != 0);
delete a1;
delete a2;
delete a3;
assert(spot::ltl::atomic_prop::instance_count() == 0);
return exit_code;
}
#!/bin/sh
. ./defs
set -e
cat >input1 <<EOF
s1, s3, a,;
s1, s2, b, p1;
s2, s1, !a,;
s2, s3, c,;
EOF
cat >input2 <<EOF
s1, s2, b, p2;
s2, s1, a, p3;
EOF
cat >input3 <<EOF
s1, s2, a,;
s1, s3, b,;
s3, s2,, p4;
s2, s3,, p4;
EOF
cat >expected <<EOF
"s1 * s1 * s1", "s3 * s2 * s2", a b, p2;
"s1 * s1 * s1", "s2 * s2 * s2", a b, p2 p1;
"s2 * s2 * s2", "s3 * s1 * s3", c a, p3 p4;
"s1 * s1 * s1", "s3 * s2 * s3", a b, p2;
"s1 * s1 * s1", "s2 * s2 * s3", b, p2 p1;
"s2 * s2 * s3", "s3 * s1 * s2", c a, p3 p4;
EOF
./tripprod input1 input2 input3 > stdout
cat stdout
diff stdout expected
rm input1 input2 input3 stdout expected
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