convert: twa to twacube translation
* spot/twacube/Makefile.am, spot/twacube/twacube.cc, spot/twacube/twacube.hh, spot/twacube_algos/convert.cc, spot/twacube_algos/convert.hh, tests/Makefile.am, tests/core/.gitignore, tests/core/twacube.cc, tests/core/twacube.test: here.
This commit is contained in:
Etienne Renault
parent
8d57700d6a
commit
aceb37ab50
9 changed files with 550 additions and 4 deletions
|
|
@ -25,8 +25,9 @@ AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
|||
|
||||
twacubedir = $(pkgincludedir)/twacube
|
||||
|
||||
twacube_HEADERS = cube.hh
|
||||
twacube_HEADERS = cube.hh twacube.hh
|
||||
|
||||
noinst_LTLIBRARIES = libtwacube.la
|
||||
libtwacube_la_SOURCES = \
|
||||
cube.cc
|
||||
cube.cc \
|
||||
twacube.cc
|
||||
|
|
|
|||
159
spot/twacube/twacube.cc
Normal file
159
spot/twacube/twacube.cc
Normal file
|
|
@ -0,0 +1,159 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2015 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 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 "twacube.hh"
|
||||
#include <iostream>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
cstate::cstate(cstate&& s) noexcept: id_(std::move(s.id_))
|
||||
{
|
||||
}
|
||||
cstate::cstate(unsigned int id): id_(id)
|
||||
{
|
||||
}
|
||||
|
||||
cstate::~cstate()
|
||||
{ }
|
||||
|
||||
unsigned int cstate::label()
|
||||
{
|
||||
return id_;
|
||||
}
|
||||
|
||||
transition::transition(transition&& t) noexcept:
|
||||
cube_(std::move(t.cube_)), acc_(std::move(t.acc_))
|
||||
{ }
|
||||
|
||||
transition::transition(const cube& cube,
|
||||
acc_cond::mark_t acc):
|
||||
cube_(cube), acc_(acc)
|
||||
{ }
|
||||
|
||||
transition::~transition()
|
||||
{ }
|
||||
|
||||
transition::transition()
|
||||
{ }
|
||||
|
||||
twacube::twacube(const std::vector<std::string>& aps):
|
||||
init_(0U), aps_(aps), cubeset_(aps.size())
|
||||
{
|
||||
}
|
||||
|
||||
twacube::~twacube()
|
||||
{
|
||||
spot::cubeset cs = get_cubeset();
|
||||
for (unsigned int i = 1; i <= theg_.num_edges(); ++i)
|
||||
cs.release(theg_.edge_data(i).cube_);
|
||||
}
|
||||
|
||||
const acc_cond& twacube::acc() const
|
||||
{
|
||||
return acc_;
|
||||
}
|
||||
|
||||
acc_cond& twacube::acc()
|
||||
{
|
||||
return acc_;
|
||||
}
|
||||
|
||||
const std::vector<std::string>& twacube::get_ap()
|
||||
{
|
||||
return aps_;
|
||||
}
|
||||
|
||||
unsigned int twacube::new_state()
|
||||
{
|
||||
return theg_.new_state();
|
||||
}
|
||||
|
||||
void twacube::set_initial(unsigned int init)
|
||||
{
|
||||
init_ = init;
|
||||
}
|
||||
|
||||
unsigned int twacube::get_initial()
|
||||
{
|
||||
if (theg_.num_states() == 0)
|
||||
new_state();
|
||||
|
||||
return init_;
|
||||
}
|
||||
|
||||
cstate* twacube::state_from_int(unsigned int i)
|
||||
{
|
||||
return &theg_.state_data(i);
|
||||
}
|
||||
|
||||
void
|
||||
twacube::create_transition(unsigned int src, const cube& cube,
|
||||
const acc_cond::mark_t& mark, unsigned int dst)
|
||||
{
|
||||
theg_.new_edge(src, dst, cube, mark);
|
||||
}
|
||||
|
||||
const cubeset&
|
||||
twacube::get_cubeset() const
|
||||
{
|
||||
return cubeset_;
|
||||
}
|
||||
|
||||
bool
|
||||
twacube::succ_contiguous() const
|
||||
{
|
||||
unsigned int i = 1;
|
||||
while (i <= theg_.num_edges())
|
||||
{
|
||||
unsigned int j = i;
|
||||
|
||||
// Walk first bucket of successors
|
||||
while (j <= theg_.num_edges() &&
|
||||
theg_.edge_storage(i).src == theg_.edge_storage(j).src)
|
||||
++j;
|
||||
|
||||
// Remove the next bucket
|
||||
unsigned int itmp = j;
|
||||
|
||||
// Look if there are some transitions missing in this bucket.
|
||||
while (j <= theg_.num_edges())
|
||||
{
|
||||
if (theg_.edge_storage(i).src == theg_.edge_storage(j).src)
|
||||
return false;
|
||||
++j;
|
||||
}
|
||||
i = itmp;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
std::ostream&
|
||||
operator<<(std::ostream& os, const twacube& twa)
|
||||
{
|
||||
spot::cubeset cs = twa.get_cubeset();
|
||||
os << "init : " << twa.init_ << '\n';
|
||||
for (unsigned int i = 1; i <= twa.theg_.num_edges(); ++i)
|
||||
os << twa.theg_.edge_storage(i).src << "->"
|
||||
<< twa.theg_.edge_storage(i).dst << " : "
|
||||
<< cs.dump(twa.theg_.edge_data(i).cube_, twa.aps_)
|
||||
<< ' ' << twa.theg_.edge_data(i).acc_
|
||||
<< '\n';
|
||||
return os;
|
||||
}
|
||||
}
|
||||
153
spot/twacube/twacube.hh
Normal file
153
spot/twacube/twacube.hh
Normal file
|
|
@ -0,0 +1,153 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2015, 2016 Laboratoire de Recherche
|
||||
// et Développement 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 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/>.
|
||||
|
||||
#pragma once
|
||||
|
||||
#include <vector>
|
||||
#include <iosfwd>
|
||||
#include <spot/graph/graph.hh>
|
||||
#include <spot/twa/acc.hh>
|
||||
#include <spot/twacube/cube.hh>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
class SPOT_API cstate
|
||||
{
|
||||
public:
|
||||
cstate() {}
|
||||
cstate(const cstate& s) = delete;
|
||||
cstate(cstate&& s) noexcept;
|
||||
cstate(unsigned int id);
|
||||
virtual ~cstate();
|
||||
unsigned int label();
|
||||
private:
|
||||
unsigned int id_;
|
||||
};
|
||||
|
||||
class SPOT_API transition
|
||||
{
|
||||
public:
|
||||
cube cube_;
|
||||
acc_cond::mark_t acc_;
|
||||
transition();
|
||||
transition(const transition& t) = delete;
|
||||
transition(transition&& t) noexcept;
|
||||
transition(const cube& cube, acc_cond::mark_t acc);
|
||||
virtual ~transition();
|
||||
};
|
||||
|
||||
class SPOT_API trans_index final
|
||||
{
|
||||
public:
|
||||
typedef digraph<cstate, transition> graph_t;
|
||||
typedef graph_t::edge_storage_t edge_storage_t;
|
||||
|
||||
trans_index(trans_index& ci) = delete;
|
||||
trans_index(unsigned int state, graph_t& g):
|
||||
st_(g.state_storage(state))
|
||||
{
|
||||
reset();
|
||||
}
|
||||
|
||||
trans_index(trans_index&& ci):
|
||||
idx_(ci.idx_),
|
||||
st_(ci.st_)
|
||||
{
|
||||
}
|
||||
|
||||
inline void reset()
|
||||
{
|
||||
idx_ = st_.succ;
|
||||
}
|
||||
|
||||
inline void next()
|
||||
{
|
||||
++idx_;
|
||||
}
|
||||
|
||||
inline bool done() const
|
||||
{
|
||||
return !idx_ || idx_ > st_.succ_tail;
|
||||
}
|
||||
|
||||
inline unsigned int current(unsigned int seed = 0) const
|
||||
{
|
||||
// no-swarming : since twacube are dedicated for parallelism, i.e.
|
||||
// swarming, we expect swarming is activated.
|
||||
if (SPOT_UNLIKELY(!seed))
|
||||
return idx_;
|
||||
// swarming.
|
||||
return (((idx_-st_.succ+1)*seed) % (st_.succ_tail-st_.succ+1)) + st_.succ;
|
||||
}
|
||||
|
||||
private:
|
||||
unsigned int idx_;
|
||||
const graph_t::state_storage_t& st_;
|
||||
};
|
||||
|
||||
class SPOT_API twacube final
|
||||
{
|
||||
public:
|
||||
twacube() = delete;
|
||||
twacube(const std::vector<std::string>& aps);
|
||||
virtual ~twacube();
|
||||
const acc_cond& acc() const;
|
||||
acc_cond& acc();
|
||||
const std::vector<std::string>& get_ap();
|
||||
unsigned int new_state();
|
||||
void set_initial(unsigned int init);
|
||||
unsigned int get_initial();
|
||||
cstate* state_from_int(unsigned int i);
|
||||
void create_transition(unsigned int src, const cube& cube,
|
||||
const acc_cond::mark_t& mark, unsigned int dst);
|
||||
const cubeset& get_cubeset() const;
|
||||
bool succ_contiguous() const;
|
||||
typedef digraph<cstate, transition> graph_t;
|
||||
const graph_t& get_graph()
|
||||
{
|
||||
return theg_;
|
||||
}
|
||||
typedef graph_t::edge_storage_t edge_storage_t;
|
||||
const graph_t::edge_storage_t&
|
||||
trans_storage(std::shared_ptr<trans_index> ci,
|
||||
unsigned int seed = 0) const
|
||||
{
|
||||
return theg_.edge_storage(ci->current(seed));
|
||||
}
|
||||
const transition& trans_data(std::shared_ptr<trans_index> ci,
|
||||
unsigned int seed = 0) const
|
||||
{
|
||||
return theg_.edge_data(ci->current(seed));
|
||||
}
|
||||
|
||||
std::shared_ptr<trans_index> succ(unsigned int i)
|
||||
{
|
||||
return std::make_shared<trans_index>(i, theg_);
|
||||
}
|
||||
|
||||
friend SPOT_API std::ostream& operator<<(std::ostream& os,
|
||||
const twacube& twa);
|
||||
private:
|
||||
unsigned int init_;
|
||||
acc_cond acc_;
|
||||
const std::vector<std::string>& aps_;
|
||||
graph_t theg_;
|
||||
cubeset cubeset_;
|
||||
};
|
||||
}
|
||||
|
|
@ -58,4 +58,76 @@ namespace spot
|
|||
}
|
||||
return result;
|
||||
}
|
||||
|
||||
spot::twacube* twa_to_twacube(spot::twa_graph_ptr& aut,
|
||||
std::unordered_map<int, int>& ap_binder,
|
||||
std::vector<std::string>& aps)
|
||||
{
|
||||
// Declare the twa cube
|
||||
spot::twacube* tg = new spot::twacube(aps);
|
||||
|
||||
// Fix acceptance
|
||||
tg->acc() = aut->acc();
|
||||
|
||||
// This binder maps twagraph indexes to twacube ones.
|
||||
std::unordered_map<int, int> st_binder;
|
||||
|
||||
// Fill binder and create corresponding states into twacube
|
||||
for (unsigned n = 0; n < aut->num_states(); ++n)
|
||||
st_binder.insert({n, tg->new_state()});
|
||||
|
||||
// Fix the initial state
|
||||
tg->set_initial(st_binder[aut->get_init_state_number()]);
|
||||
|
||||
// Get the cubeset
|
||||
auto cs = tg->get_cubeset();
|
||||
|
||||
// Now just build all transitions of this automaton
|
||||
// spot::cube cube(aps);
|
||||
for (unsigned n = 0; n < aut->num_states(); ++n)
|
||||
for (auto& t: aut->out(n))
|
||||
{
|
||||
bdd cond = t.cond;
|
||||
|
||||
// Special case for bddfalse
|
||||
if (cond == bddfalse)
|
||||
{
|
||||
spot::cube cube = tg->get_cubeset().alloc();
|
||||
for (unsigned int i = 0; i < cs.size(); ++i)
|
||||
cs.set_false_var(cube, i); // FIXME ! use fill!
|
||||
tg->create_transition(st_binder[n], cube,
|
||||
t.acc, st_binder[t.dst]);
|
||||
}
|
||||
else
|
||||
// Split the bdd into multiple transitions
|
||||
while (cond != bddfalse)
|
||||
{
|
||||
bdd one = bdd_satone(cond);
|
||||
cond -= one;
|
||||
spot::cube cube =spot::satone_to_cube(one, cs, ap_binder);
|
||||
tg->create_transition(st_binder[n], cube, t.acc,
|
||||
st_binder[t.dst]);
|
||||
}
|
||||
}
|
||||
// Must be contiguous to support swarming.
|
||||
assert(tg->succ_contiguous());
|
||||
return tg;
|
||||
}
|
||||
|
||||
std::vector<std::string>*
|
||||
extract_aps(spot::twa_graph_ptr& aut,
|
||||
std::unordered_map<int, int>& ap_binder)
|
||||
{
|
||||
std::vector<std::string>* aps = new std::vector<std::string>();
|
||||
for (auto f: aut->ap())
|
||||
{
|
||||
int size = aps->size();
|
||||
if (std::find(aps->begin(), aps->end(), f.ap_name()) == aps->end())
|
||||
{
|
||||
aps->push_back(f.ap_name());
|
||||
ap_binder.insert({aut->get_dict()->var_map[f], size});
|
||||
}
|
||||
}
|
||||
return aps;
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -24,6 +24,8 @@
|
|||
#include <unordered_map>
|
||||
#include <spot/misc/common.hh>
|
||||
#include <spot/twacube/cube.hh>
|
||||
#include <spot/twacube/twacube.hh>
|
||||
#include <spot/twa/twagraph.hh>
|
||||
|
||||
namespace spot
|
||||
{
|
||||
|
|
@ -37,4 +39,15 @@ namespace spot
|
|||
/// that bind cube indexes to bdd indexes.
|
||||
SPOT_API bdd cube_to_bdd(spot::cube cube, const cubeset& cubeset,
|
||||
std::unordered_map<int, int>& reverse_binder);
|
||||
|
||||
/// \brief Extract the atomic propositions from the automaton
|
||||
SPOT_API std::vector<std::string>*
|
||||
extract_aps(spot::twa_graph_ptr& aut,
|
||||
std::unordered_map<int, int>& ap_binder);
|
||||
|
||||
/// \brief Convert a twa into a twacube
|
||||
SPOT_API spot::twacube*
|
||||
twa_to_twacube(spot::twa_graph_ptr& aut,
|
||||
std::unordered_map<int, int>& ap_binder,
|
||||
std::vector<std::string>& aps);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -99,7 +99,8 @@ check_PROGRAMS = \
|
|||
core/tgbagraph \
|
||||
core/tostring \
|
||||
core/tunabbrev \
|
||||
core/tunenoform
|
||||
core/tunenoform \
|
||||
core/twacube
|
||||
|
||||
# Keep this sorted alphabetically.
|
||||
core_acc_SOURCES = core/acc.cc
|
||||
|
|
@ -150,6 +151,7 @@ core_tunabbrev_SOURCES = core/equalsf.cc
|
|||
core_tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DUNABBREV='"^ieFG"'
|
||||
core_tunenoform_SOURCES = core/equalsf.cc
|
||||
core_tunenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM -DUNABBREV='"^ieFG"'
|
||||
core_twacube_SOURCES = core/twacube.cc
|
||||
|
||||
|
||||
TESTS_tl = \
|
||||
|
|
@ -328,7 +330,8 @@ TESTS_twa = \
|
|||
core/parity.test \
|
||||
core/parity2.test \
|
||||
core/ltlsynt.test \
|
||||
core/rabin2parity.test
|
||||
core/rabin2parity.test \
|
||||
core/twacube.test
|
||||
|
||||
############################## PYTHON ##############################
|
||||
|
||||
|
|
|
|||
1
tests/core/.gitignore
vendored
1
tests/core/.gitignore
vendored
|
|
@ -74,5 +74,6 @@ tripprod
|
|||
trival
|
||||
tunabbrev
|
||||
tunenoform
|
||||
twacube
|
||||
unabbrevwm
|
||||
safra
|
||||
|
|
|
|||
73
tests/core/twacube.cc
Normal file
73
tests/core/twacube.cc
Normal file
|
|
@ -0,0 +1,73 @@
|
|||
// -*- coding: utf-8 -*-
|
||||
// Copyright (C) 2015, 2016 Laboratoire de Recherche et Développement
|
||||
// de l'Epita.
|
||||
//
|
||||
// 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 <bddx.h>
|
||||
|
||||
#include <iostream>
|
||||
#include <spot/twacube/twacube.hh>
|
||||
#include <spot/twacube_algos/convert.hh>
|
||||
#include <iostream>
|
||||
#include <spot/twa/twagraph.hh>
|
||||
#include <spot/twaalgos/dot.hh>
|
||||
#include <spot/tl/defaultenv.hh>
|
||||
|
||||
int main()
|
||||
{
|
||||
// Build some TWA
|
||||
auto d = spot::make_bdd_dict();
|
||||
auto tg = make_twa_graph(d);
|
||||
bdd p1 = bdd_ithvar(tg->register_ap("p1"));
|
||||
bdd p2 = bdd_ithvar(tg->register_ap("p2"));
|
||||
tg->acc().add_sets(2);
|
||||
auto s1 = tg->new_state();
|
||||
auto s2 = tg->new_state();
|
||||
auto s3 = tg->new_state();
|
||||
tg->new_edge(s1, s1, bddfalse, 0U);
|
||||
tg->new_edge(s1, s2, p1, 0U);
|
||||
tg->new_edge(s1, s3, p2, tg->acc().mark(1));
|
||||
tg->new_edge(s2, s3, p1 & p2, tg->acc().mark(0));
|
||||
tg->new_edge(s3, s1, p1 | p2, spot::acc_cond::mark_t({0, 1}));
|
||||
tg->new_edge(s3, s2, p1 >> p2, 0U);
|
||||
tg->new_edge(s3, s3, bddtrue, spot::acc_cond::mark_t({0, 1}));
|
||||
|
||||
// Map Bdd indexes to cube indexes
|
||||
std::unordered_map<int, int> ap_binder;
|
||||
|
||||
// Get the set of propositions used by this automaton
|
||||
std::vector<std::string>* aps = extract_aps(tg, ap_binder);
|
||||
|
||||
// Test translation
|
||||
auto* aut = twa_to_twacube(tg, ap_binder, *aps);
|
||||
spot::print_dot(std::cout, tg);
|
||||
std::cout << "-----------\n" << *aut << "-----------\n";
|
||||
|
||||
unsigned int seed = 17;
|
||||
for (auto it = aut->succ(2); !it->done(); it->next())
|
||||
{
|
||||
auto& t = aut->trans_storage(it, seed);
|
||||
auto& d = aut->trans_data(it, seed);
|
||||
std::cout << t.src << ' ' << t.dst << ' '
|
||||
<< ' ' << aut->get_cubeset().dump(d.cube_, *aps)
|
||||
<< ' ' << d.acc_
|
||||
<< std::endl;
|
||||
}
|
||||
|
||||
delete aps;
|
||||
delete aut;
|
||||
}
|
||||
71
tests/core/twacube.test
Executable file
71
tests/core/twacube.test
Executable file
|
|
@ -0,0 +1,71 @@
|
|||
#!/bin/sh
|
||||
# -*- coding: utf-8 -*-
|
||||
# Copyright (C) 2014, 2015 Laboratoire de Recherche et Développement 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 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/>.
|
||||
|
||||
# While running some benchmark, Tomáš Babiak found that Spot took too
|
||||
# much time (i.e. >1h) to translate those six formulae. It turns out
|
||||
# that the WDBA minimization was performed after the degeneralization
|
||||
# algorithm, while this is not necessary (WDBA will produce a BA, so
|
||||
# we may as well skip degeneralization). Translating these formulae
|
||||
# in the test-suite ensure that they don't take too much time (the
|
||||
# buildfarm will timeout if it does).
|
||||
|
||||
. ./defs
|
||||
|
||||
set -e
|
||||
|
||||
run 0 ../twacube > stdout
|
||||
|
||||
cat >expected <<EOF
|
||||
digraph G {
|
||||
rankdir=LR
|
||||
node [shape="circle"]
|
||||
I [label="", style=invis, width=0]
|
||||
I -> 0
|
||||
0 [label="0"]
|
||||
0 -> 0 [label="0"]
|
||||
0 -> 1 [label="p1"]
|
||||
0 -> 2 [label="p2\n{1}"]
|
||||
1 [label="1"]
|
||||
1 -> 2 [label="p1 & p2\n{0}"]
|
||||
2 [label="2"]
|
||||
2 -> 0 [label="p1 | p2\n{0,1}"]
|
||||
2 -> 1 [label="!p1 | p2"]
|
||||
2 -> 2 [label="1\n{0,1}"]
|
||||
}
|
||||
-----------
|
||||
init : 0
|
||||
0->0 : !p1&!p2 {}
|
||||
0->1 : p1 {}
|
||||
0->2 : p2 {1}
|
||||
1->2 : p1&p2 {0}
|
||||
2->0 : !p1&p2 {0,1}
|
||||
2->0 : p1 {0,1}
|
||||
2->1 : !p1 {}
|
||||
2->1 : p1&p2 {}
|
||||
2->2 : 1 {0,1}
|
||||
-----------
|
||||
2 1 !p1 {}
|
||||
2 2 1 {0,1}
|
||||
2 0 p1 {0,1}
|
||||
2 1 p1&p2 {}
|
||||
2 0 !p1&p2 {0,1}
|
||||
EOF
|
||||
|
||||
diff stdout expected
|
||||
Loading…
Add table
Add a link
Reference in a new issue