Delete the cutscc algorithms.
These were used in old experiments, but have not turned useful in practice. Not worth keeping and maintaining. * src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh: Delete. * bench/scc-stats/, bench/split-product/: Delete. * configure.ac, src/tgbaalgos/Makefile.am, README, bench/Makefile.am: Adjust.
This commit is contained in:
Alexandre Duret-Lutz
parent
1a93166d15
commit
401179eae7
30 changed files with 2 additions and 2740 deletions
2
README
2
README
|
|
@ -181,8 +181,6 @@ bench/ Benchmarks for ...
|
||||||
ltl2tgba/ ... LTL-to-Büchi translation algorithms,
|
ltl2tgba/ ... LTL-to-Büchi translation algorithms,
|
||||||
ltlcounter/ ... translation of a class of LTL formulae,
|
ltlcounter/ ... translation of a class of LTL formulae,
|
||||||
ltlclasses/ ... translation of more classes of LTL formulae,
|
ltlclasses/ ... translation of more classes of LTL formulae,
|
||||||
scc-stats/ ... SCC statistics after translation of LTL formulae,
|
|
||||||
split-product/ ... parallelizing gain after splitting LTL automata,
|
|
||||||
spin13/ ... compositional suspension and other improvements,
|
spin13/ ... compositional suspension and other improvements,
|
||||||
wdba/ ... WDBA minimization (for obligation properties).
|
wdba/ ... WDBA minimization (for obligation properties).
|
||||||
wrap/ Wrappers for other languages.
|
wrap/ Wrappers for other languages.
|
||||||
|
|
|
||||||
|
|
@ -1,4 +1,4 @@
|
||||||
## Copyright (C) 2008, 2009, 2010, 2012, 2013 Laboratoire de Recherche
|
## Copyright (C) 2008, 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche
|
||||||
## et Développement de l'Epita (LRDE).
|
## et Développement de l'Epita (LRDE).
|
||||||
## Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
## Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||||
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||||
|
|
@ -19,5 +19,4 @@
|
||||||
## You should have received a copy of the GNU General Public License
|
## You should have received a copy of the GNU General Public License
|
||||||
## along with this program. If not, see <http://www.gnu.org/licenses/>.
|
## along with this program. If not, see <http://www.gnu.org/licenses/>.
|
||||||
|
|
||||||
SUBDIRS = emptchk ltl2tgba scc-stats split-product ltlcounter \
|
SUBDIRS = emptchk ltl2tgba ltlcounter ltlclasses wdba spin13 dtgbasat
|
||||||
ltlclasses wdba spin13 dtgbasat
|
|
||||||
|
|
|
||||||
|
|
@ -1,29 +0,0 @@
|
||||||
## Copyright (C) 2009 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/>.
|
|
||||||
|
|
||||||
AM_CPPFLAGS = -I$(srcdir)/../../src $(BUDDY_CPPFLAGS)
|
|
||||||
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
|
||||||
LDADD = ../../src/libspot.la
|
|
||||||
|
|
||||||
noinst_PROGRAMS = \
|
|
||||||
stats
|
|
||||||
|
|
||||||
stats_SOURCES = stats.cc
|
|
||||||
|
|
||||||
bench: $(noinst_PROGRAMS)
|
|
||||||
./stats $(srcdir)/formulae.ltl
|
|
||||||
|
|
@ -1,103 +0,0 @@
|
||||||
This directory contains the input files and test program used to compute basic
|
|
||||||
statistics on TGBA.
|
|
||||||
|
|
||||||
==========
|
|
||||||
CONTENTS
|
|
||||||
==========
|
|
||||||
|
|
||||||
This directory contains:
|
|
||||||
|
|
||||||
* formulae.ltl
|
|
||||||
|
|
||||||
A list of 96 handwritten formulae with their negations. They come
|
|
||||||
from three sources:
|
|
||||||
|
|
||||||
@InProceedings{ dwyer.98.fmsp,
|
|
||||||
author = {Matthew B. Dwyer and George S. Avrunin and James C.
|
|
||||||
Corbett},
|
|
||||||
title = {Property Specification Patterns for Finite-state
|
|
||||||
Verification},
|
|
||||||
booktitle = {Proceedings of the 2nd Workshop on Formal Methods in
|
|
||||||
Software Practice (FMSP'98)},
|
|
||||||
publisher = {ACM Press},
|
|
||||||
address = {New York},
|
|
||||||
editor = {Mark Ardis},
|
|
||||||
month = mar,
|
|
||||||
year = {1998},
|
|
||||||
pages = {7--15}
|
|
||||||
}
|
|
||||||
|
|
||||||
@InProceedings{ etessami.00.concur,
|
|
||||||
author = {Kousha Etessami and Gerard J. Holzmann},
|
|
||||||
title = {Optimizing {B\"u}chi Automata},
|
|
||||||
booktitle = {Proceedings of the 11th International Conference on
|
|
||||||
Concurrency Theory (Concur'00)},
|
|
||||||
pages = {153--167},
|
|
||||||
year = {2000},
|
|
||||||
editor = {C. Palamidessi},
|
|
||||||
volume = {1877},
|
|
||||||
series = {Lecture Notes in Computer Science},
|
|
||||||
address = {Pennsylvania, USA},
|
|
||||||
publisher = {Springer-Verlag}
|
|
||||||
}
|
|
||||||
|
|
||||||
@InProceedings{ somenzi.00.cav,
|
|
||||||
author = {Fabio Somenzi and Roderick Bloem},
|
|
||||||
title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}},
|
|
||||||
booktitle = {Proceedings of the 12th International Conference on
|
|
||||||
Computer Aided Verification (CAV'00)},
|
|
||||||
pages = {247--263},
|
|
||||||
year = {2000},
|
|
||||||
volume = {1855},
|
|
||||||
series = {Lecture Notes in Computer Science},
|
|
||||||
address = {Chicago, Illinois, USA},
|
|
||||||
publisher = {Springer-Verlag}
|
|
||||||
}
|
|
||||||
|
|
||||||
* full.ltl
|
|
||||||
|
|
||||||
A list of 1000 large randomly generated LTL formulae with ./randtgba.
|
|
||||||
|
|
||||||
=======
|
|
||||||
USAGE
|
|
||||||
=======
|
|
||||||
|
|
||||||
Use the stats program.
|
|
||||||
Usage : ./stats ltl_file
|
|
||||||
Where ltl_file is a file with a single LTL formula per line.
|
|
||||||
|
|
||||||
==========================
|
|
||||||
INTERPRETING THE RESULTS
|
|
||||||
==========================
|
|
||||||
|
|
||||||
Results can be found in file 'results'.
|
|
||||||
Here is the list of the measured values:
|
|
||||||
- Accepting Strongly Connected Components.
|
|
||||||
Total number of accepting SCC.
|
|
||||||
- Dead Strongly Connected Components.
|
|
||||||
Total number of dead SCC.
|
|
||||||
An SCC is dead if no accepting SCC is reachable from it.
|
|
||||||
- Accepting Paths.
|
|
||||||
Number of maximal accepting paths.
|
|
||||||
An path is maximal and accepting if it ends in an accepting
|
|
||||||
SCC that is only dead (i.e. non accepting) successors, or no
|
|
||||||
successors at all.
|
|
||||||
- Dead Paths.
|
|
||||||
Number of paths to a terminal dead SCC.
|
|
||||||
A terminal dead SCC is a dead SCC without successors.
|
|
||||||
- Max Effective Splitting.
|
|
||||||
A clue to measure the potential effectiveness of splitting the formula.
|
|
||||||
This is the maximum number of possible sub automata with unique states.
|
|
||||||
Beyond this threshold, more sub automata can be generated, but all their
|
|
||||||
states will be included in some of the previous automata.
|
|
||||||
- Self Loops per State.
|
|
||||||
Number of self loops.
|
|
||||||
A self loop is a transition from a state to itself.
|
|
||||||
|
|
||||||
For each of these measured value, we provide the following statistics
|
|
||||||
computed on all the formulae in ltl_file:\
|
|
||||||
- Min
|
|
||||||
- Max
|
|
||||||
- Mean
|
|
||||||
- Median
|
|
||||||
- Standard Deviation
|
|
||||||
|
|
@ -1,55 +0,0 @@
|
||||||
[](!p0)
|
|
||||||
<>p1 -> (!p0 U p1)
|
|
||||||
[](p2 -> [](!p0))
|
|
||||||
[]((p2 & !p1 & <>p1) -> (!p0 U p1))
|
|
||||||
[](p2 & !p1 -> (!p0 U (p1 | []!p0)))
|
|
||||||
<>(p0)
|
|
||||||
!p1 U ((p0 & !p1) | []!p1)
|
|
||||||
[](!p2) | <>(p2 & <>p0)
|
|
||||||
[](p2 & !p1 -> (!p1 U ((p0 & !p1) | []!p1)))
|
|
||||||
[](p2 & !p1 -> (!p1 U (p0 & !p1)))
|
|
||||||
<>p1 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1)))))))))
|
|
||||||
[]((p2 & <>p1) -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1))))))))))
|
|
||||||
[](p2 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U (p1 | []!p0)) | []p0)))))))))
|
|
||||||
[](p0)
|
|
||||||
<>p1 -> (p0 U p1)
|
|
||||||
[](p2 -> [](p0))
|
|
||||||
[]((p2 & !p1 & <>p1) -> (p0 U p1))
|
|
||||||
[](p2 & !p1 -> (p0 U (p1 | [] p0)))
|
|
||||||
!p0 U (p3 | []!p0)
|
|
||||||
<>p1 -> (!p0 U (p3 | p1))
|
|
||||||
[]!p2 | <>(p2 & (!p0 U (p3 | []!p0)))
|
|
||||||
[]((p2 & !p1 & <>p1) -> (!p0 U (p3 | p1)))
|
|
||||||
[](p2 & !p1 -> (!p0 U ((p3 | p1) | []!p0)))
|
|
||||||
[](p0 -> <>p3)
|
|
||||||
<>p1 -> (p0 -> (!p1 U (p3 & !p1))) U p1
|
|
||||||
[](p2 -> [](p0 -> <>p3))
|
|
||||||
[]((p2 & !p1 & <>p1) -> (p0 -> (!p1 U (p3 & !p1))) U p1)
|
|
||||||
[](p2 & !p1 -> ((p0 -> (!p1 U (p3 & !p1))) U (p1 | [](p0 -> (!p1 U (p3 & !p1))))))
|
|
||||||
<>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))
|
|
||||||
<>p1 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))
|
|
||||||
([]!p2) | (!p2 U (p2 & <>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))))
|
|
||||||
[]((p2 & <>p1) -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4)))))
|
|
||||||
[](p2 -> (<>p0 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))))
|
|
||||||
(<>(p3 & X<>p4)) -> ((!p3) U p0)
|
|
||||||
<>p1 -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0))
|
|
||||||
([]!p2) | ((!p2) U (p2 & ((<>(p3 & X<>p4)) -> ((!p3) U p0))))
|
|
||||||
[]((p2 & <>p1) -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0)))
|
|
||||||
[](p2 -> (!(p3 & (!p1) & X(!p1 U (p4 & !p1))) U (p1 | p0) | [](!(p3 & X<>p4))))
|
|
||||||
[] (p3 & X<> p4 -> X(<>(p4 & <> p0)))
|
|
||||||
<>p1 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1
|
|
||||||
[] (p2 -> [] (p3 & X<> p4 -> X(!p4 U (p4 & <> p0))))
|
|
||||||
[] ((p2 & <>p1) -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1)
|
|
||||||
[] (p2 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U (p1 | [] (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0)))))
|
|
||||||
[] (p0 -> <>(p3 & X<>p4))
|
|
||||||
<>p1 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1
|
|
||||||
[] (p2 -> [] (p0 -> (p3 & X<> p4)))
|
|
||||||
[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1)
|
|
||||||
[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U (p1 | [] (p0 -> (p3 & X<> p4))))
|
|
||||||
[] (p0 -> <>(p3 & !p5 & X(!p5 U p4)))
|
|
||||||
<>p1 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1
|
|
||||||
[] (p2 -> [] (p0 -> (p3 & !p5 & X(!p5 U p4))))
|
|
||||||
[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1)
|
|
||||||
[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U (p1 | [] (p0 -> (p3 & !p5 & X(!p5 U p4)))))
|
|
||||||
!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0)
|
|
||||||
<>p2 -> (!p2 U (p2 & (!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0))))
|
|
||||||
|
|
@ -1,203 +0,0 @@
|
||||||
// -*- coding: utf-8 -*-
|
|
||||||
// Copyright (C) 2009, 2010, 2012, 2013 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/>.
|
|
||||||
|
|
||||||
#include <queue>
|
|
||||||
#include <math.h>
|
|
||||||
#include "tgbaalgos/scc.hh"
|
|
||||||
#include "tgbaalgos/cutscc.hh"
|
|
||||||
#include "ltlparse/ltlfile.hh"
|
|
||||||
#include "tgbaalgos/ltl2tgba_fm.hh"
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
unsigned tgba_size(const tgba* a)
|
|
||||||
{
|
|
||||||
typedef std::unordered_set<const state*,
|
|
||||||
state_ptr_hash, state_ptr_equal> hash_type;
|
|
||||||
hash_type seen;
|
|
||||||
std::queue<state*> tovisit;
|
|
||||||
// Perform breadth-first search.
|
|
||||||
state* init = a->get_init_state();
|
|
||||||
tovisit.push(init);
|
|
||||||
seen.insert(init);
|
|
||||||
unsigned count = 0;
|
|
||||||
// While there are still states to visit.
|
|
||||||
while (!tovisit.empty())
|
|
||||||
{
|
|
||||||
++count;
|
|
||||||
state* cur = tovisit.front();
|
|
||||||
tovisit.pop();
|
|
||||||
tgba_succ_iterator* sit = a->succ_iter(cur);
|
|
||||||
for (sit->first(); !sit->done(); sit->next())
|
|
||||||
{
|
|
||||||
state* dst = sit->current_state();
|
|
||||||
// Is it a new state ?
|
|
||||||
if (seen.find(dst) == seen.end())
|
|
||||||
{
|
|
||||||
// Yes, register the successor for later processing.
|
|
||||||
tovisit.push(dst);
|
|
||||||
seen.insert(dst);
|
|
||||||
}
|
|
||||||
else
|
|
||||||
// No, free dst.
|
|
||||||
dst->destroy();
|
|
||||||
}
|
|
||||||
delete sit;
|
|
||||||
}
|
|
||||||
hash_type::iterator it2;
|
|
||||||
// Free visited states.
|
|
||||||
for (it2 = seen.begin(); it2 != seen.end(); it2++)
|
|
||||||
(*it2)->destroy();
|
|
||||||
return count;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void compute_and_print(std::vector<double>& v,
|
|
||||||
int count, std::ofstream& output)
|
|
||||||
{
|
|
||||||
int i;
|
|
||||||
double sum = 0.;
|
|
||||||
double mean;
|
|
||||||
double median;
|
|
||||||
double variance = 0.;
|
|
||||||
sum = 0;
|
|
||||||
// Compute mean: sigma(Xi)/n for i=0..n-1.
|
|
||||||
for (i = 0; i < count; i++)
|
|
||||||
sum += v[i];
|
|
||||||
mean = sum / count;
|
|
||||||
// Compute variance: sigma((Xi - mean)*(Xi - mean))/n for i=0..n-1.
|
|
||||||
for (i = 0; i < count; i++)
|
|
||||||
variance += (v[i] - mean)*(v[i] - mean);
|
|
||||||
variance = variance / count;
|
|
||||||
// Compute median: mean of (n-th/2) value and ((n-th/2)+1) value if n even
|
|
||||||
// else (n-th+1) value if n odd.
|
|
||||||
if (count % 2 == 0)
|
|
||||||
median = float(v[count/2] + v[(count/2)+1])/2;
|
|
||||||
else
|
|
||||||
median = v[(count+1)/2];
|
|
||||||
output << "\tMin = " << v[0] << std::endl;
|
|
||||||
output << "\tMax = " << v[count-1] << std::endl;
|
|
||||||
output << "\tMean = " << mean << std::endl;
|
|
||||||
output << "\tMedian = " << median << std::endl;
|
|
||||||
output << "\tStandard Deviation = " << sqrt(variance) << std::endl;
|
|
||||||
output << std::endl;
|
|
||||||
}
|
|
||||||
|
|
||||||
int main (int argc, char* argv[])
|
|
||||||
{
|
|
||||||
if (argc != 2)
|
|
||||||
{
|
|
||||||
std::cout << "Usage : ./stats file_name" << std::endl;
|
|
||||||
std::cout << "There must be one LTL formula per line." << std::endl;
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
std::ofstream output;
|
|
||||||
output.open("results");
|
|
||||||
spot::bdd_dict* dict = new spot::bdd_dict();
|
|
||||||
unsigned count = 0;
|
|
||||||
std::vector<double> acc_scc;
|
|
||||||
std::vector<double> dead_scc;
|
|
||||||
std::vector<double> acc_paths;
|
|
||||||
std::vector<double> dead_paths;
|
|
||||||
std::vector<double> spanning_paths;
|
|
||||||
std::vector<double> self_loops;
|
|
||||||
unsigned k = 0;
|
|
||||||
// Get each LTL formula.
|
|
||||||
spot::ltl::ltl_file formulae(argv[1]);
|
|
||||||
while (const spot::ltl::formula* f = formulae.next())
|
|
||||||
{
|
|
||||||
++k;
|
|
||||||
spot::tgba* a = ltl_to_tgba_fm(f, dict, /* exprop */ true);
|
|
||||||
f->destroy();
|
|
||||||
// Get number of spanning paths.
|
|
||||||
spot::scc_map m (a);
|
|
||||||
m.build_map();
|
|
||||||
spot::state* initial_state = a->get_init_state();
|
|
||||||
unsigned init = m.scc_of_state(initial_state);
|
|
||||||
initial_state->destroy();
|
|
||||||
std::vector<std::vector<spot::sccs_set* > >* paths = find_paths(a, m);
|
|
||||||
unsigned spanning_count =spot::max_spanning_paths(&(*paths)[init], m);
|
|
||||||
spanning_paths.push_back(double(spanning_count));
|
|
||||||
// Get characteristics from automaton.
|
|
||||||
spot::scc_stats stat;
|
|
||||||
stat = build_scc_stats(a);
|
|
||||||
|
|
||||||
// Add those characteristics to our arrays.
|
|
||||||
acc_scc.push_back(double(stat.acc_scc));
|
|
||||||
dead_scc.push_back(double(stat.dead_scc));
|
|
||||||
acc_paths.push_back(double(stat.acc_paths));
|
|
||||||
dead_paths.push_back(double(stat.dead_paths));
|
|
||||||
self_loops.push_back(double(stat.self_loops)/tgba_size(a));
|
|
||||||
++count;
|
|
||||||
delete a;
|
|
||||||
unsigned i;
|
|
||||||
unsigned j;
|
|
||||||
for (i = 0; i < paths->size(); ++i)
|
|
||||||
for (j = 0; j < (*paths)[i].size(); ++j)
|
|
||||||
delete (*paths)[i][j];
|
|
||||||
delete paths;
|
|
||||||
}
|
|
||||||
|
|
||||||
if (count == 0)
|
|
||||||
{
|
|
||||||
std::cerr << "Nothing read." << std::endl;
|
|
||||||
exit(1);
|
|
||||||
}
|
|
||||||
|
|
||||||
// We could have inserted at the right place instead of
|
|
||||||
// sorting at the end.
|
|
||||||
// Sorting allows us to find the extrema and
|
|
||||||
// the median of the distribution.
|
|
||||||
sort(acc_scc.begin(), acc_scc.end());
|
|
||||||
sort(dead_scc.begin(), dead_scc.end());
|
|
||||||
sort(acc_paths.begin(), acc_paths.end());
|
|
||||||
sort(spanning_paths.begin(), spanning_paths.end());
|
|
||||||
sort(dead_paths.begin(), dead_paths.end());
|
|
||||||
sort(self_loops.begin(), self_loops.end());
|
|
||||||
output << "Parsed Formulae : " << count << std::endl << std::endl;
|
|
||||||
|
|
||||||
// Accepting SCCs
|
|
||||||
output << "Accepting SCCs:" << std::endl;
|
|
||||||
compute_and_print(acc_scc, count, output);
|
|
||||||
|
|
||||||
// Dead SCCs
|
|
||||||
output << "Dead SCCs:" << std::endl;
|
|
||||||
compute_and_print(dead_scc, count, output);
|
|
||||||
|
|
||||||
// Accepting Paths
|
|
||||||
output << "Accepting Paths:" << std::endl;
|
|
||||||
compute_and_print(acc_paths, count, output);
|
|
||||||
|
|
||||||
// Dead Paths
|
|
||||||
output << "Dead Paths:" << std::endl;
|
|
||||||
compute_and_print(dead_paths, count, output);
|
|
||||||
|
|
||||||
// Max Effective Splitting
|
|
||||||
output << "Max effective splitting:" << std::endl;
|
|
||||||
compute_and_print(spanning_paths, count, output);
|
|
||||||
|
|
||||||
// Self loops
|
|
||||||
output << "Self loops per State:" << std::endl;
|
|
||||||
compute_and_print(self_loops, count, output);
|
|
||||||
|
|
||||||
std::cout << "Statistics generated in file results." << std::endl;
|
|
||||||
output.close();
|
|
||||||
delete dict;
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
@ -1,148 +0,0 @@
|
||||||
## Copyright (C) 2009, 2010 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/>.
|
|
||||||
|
|
||||||
PML2TGBA = $(PERL) $(srcdir)/pml2tgba.pl
|
|
||||||
|
|
||||||
RES = cut-results
|
|
||||||
|
|
||||||
AM_CPPFLAGS = -I$(srcdir)/../../src $(BUDDY_CPPFLAGS)
|
|
||||||
AM_CXXFLAGS = $(WARNING_CXXFLAGS)
|
|
||||||
LDADD = ../../src/libspot.la
|
|
||||||
|
|
||||||
dist_noinst_SCRIPTS = \
|
|
||||||
pml2tgba.pl
|
|
||||||
|
|
||||||
noinst_PROGRAMS = \
|
|
||||||
cutscc
|
|
||||||
|
|
||||||
cutscc_SOURCES = cutscc.cc
|
|
||||||
|
|
||||||
nodist_noinst_DATA = \
|
|
||||||
models/cl3serv1.tgba \
|
|
||||||
models/cl3serv1R.tgba \
|
|
||||||
models/cl3serv3.tgba \
|
|
||||||
models/cl3serv3R.tgba \
|
|
||||||
models/eeaean1.tgba \
|
|
||||||
models/eeaean1R.tgba \
|
|
||||||
models/eeaean2.tgba \
|
|
||||||
models/eeaean2R.tgba \
|
|
||||||
models/leader.tgba \
|
|
||||||
models/leaderR.tgba \
|
|
||||||
models/mobile1.tgba \
|
|
||||||
models/mobile1R.tgba \
|
|
||||||
models/mobile2.tgba \
|
|
||||||
models/mobile2R.tgba \
|
|
||||||
models/zune.tgba \
|
|
||||||
models/zuneR.tgba
|
|
||||||
|
|
||||||
models/cl3serv1.tgba: $(srcdir)/models/cl3serv1.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) $(srcdir)/models/cl3serv1.pml w1 s1 >$@
|
|
||||||
|
|
||||||
models/cl3serv1R.tgba: $(srcdir)/models/cl3serv1.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) -r $(srcdir)/models/cl3serv1.pml w1 s1 >$@
|
|
||||||
|
|
||||||
models/cl3serv3.tgba: $(srcdir)/models/cl3serv3.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) $(srcdir)/models/cl3serv3.pml w1 s1 >$@
|
|
||||||
|
|
||||||
models/cl3serv3R.tgba: $(srcdir)/models/cl3serv3.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) -r $(srcdir)/models/cl3serv3.pml w1 s1 >$@
|
|
||||||
|
|
||||||
models/eeaean1.tgba: $(srcdir)/models/eeaean1.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) $(srcdir)/models/eeaean1.pml \
|
|
||||||
noLeader zeroLeads oneLeads twoLeads threeLeads >$@
|
|
||||||
|
|
||||||
models/eeaean1R.tgba: $(srcdir)/models/eeaean1.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) -r $(srcdir)/models/eeaean1.pml \
|
|
||||||
noLeader zeroLeads oneLeads twoLeads threeLeads >$@
|
|
||||||
|
|
||||||
models/eeaean2.tgba: $(srcdir)/models/eeaean2.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) $(srcdir)/models/eeaean2.pml \
|
|
||||||
noLeader zeroLeads oneLeads twoLeads threeLeads >$@
|
|
||||||
|
|
||||||
models/eeaean2R.tgba: $(srcdir)/models/eeaean2.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) -r $(srcdir)/models/eeaean2.pml \
|
|
||||||
noLeader zeroLeads oneLeads twoLeads threeLeads >$@
|
|
||||||
|
|
||||||
models/leader.tgba: $(srcdir)/models/leader.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) $(srcdir)/models/leader.pml \
|
|
||||||
elected noLeader oneLeader >$@
|
|
||||||
|
|
||||||
models/leaderR.tgba: $(srcdir)/models/leader.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) -r $(srcdir)/models/leader.pml \
|
|
||||||
elected noLeader oneLeader >$@
|
|
||||||
|
|
||||||
models/mobile1.tgba: $(srcdir)/models/mobile1.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) $(srcdir)/models/mobile1.pml \
|
|
||||||
p q r >$@
|
|
||||||
|
|
||||||
models/mobile1R.tgba: $(srcdir)/models/mobile1.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) -r $(srcdir)/models/mobile1.pml \
|
|
||||||
p q r >$@
|
|
||||||
|
|
||||||
models/mobile2.tgba: $(srcdir)/models/mobile2.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) $(srcdir)/models/mobile2.pml \
|
|
||||||
p q r >$@
|
|
||||||
|
|
||||||
models/mobile2R.tgba: $(srcdir)/models/mobile2.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) -r $(srcdir)/models/mobile2.pml \
|
|
||||||
p q r >$@
|
|
||||||
|
|
||||||
models/zune.tgba: $(srcdir)/models/zune.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) $(srcdir)/models/zune.pml \
|
|
||||||
zune_at_S zune_at_E >$@
|
|
||||||
|
|
||||||
models/zuneR.tgba: $(srcdir)/models/zune.pml
|
|
||||||
$(mkdir_p) models
|
|
||||||
$(PML2TGBA) -r $(srcdir)/models/zune.pml \
|
|
||||||
zune_at_S zune_at_E >$@
|
|
||||||
|
|
||||||
CLEANFILES = $(nodist_noinst_DATA)
|
|
||||||
|
|
||||||
bench: $(noinst_PROGRAMS)
|
|
||||||
mkdir cut-results 2> /dev/null || true
|
|
||||||
./cutscc models/clserv.ltl 4 models/cl3serv1.tgba > $(RES)/cl3serv1
|
|
||||||
./cutscc models/clserv.ltl 4 models/cl3serv1R.tgba > $(RES)/cl3serv1R
|
|
||||||
./cutscc models/clserv.ltl 4 models/cl3serv3.tgba > $(RES)/cl3serv3
|
|
||||||
./cutscc models/clserv.ltl 4 models/cl3serv3R.tgba > $(RES)/cl3serv3R
|
|
||||||
./cutscc models/eeaean.ltl 4 models/eeaean1.tgba > $(RES)/eeaean1
|
|
||||||
./cutscc models/eeaean.ltl 4 models/eeaean1R.tgba > $(RES)/eeaean1R
|
|
||||||
./cutscc models/eeaean.ltl 4 models/eeaean2.tgba > $(RES)/eeaean2
|
|
||||||
./cutscc models/eeaean.ltl 4 models/eeaean2R.tgba > $(RES)/eeaean2R
|
|
||||||
./cutscc models/leader.ltl 4 models/leader.tgba > $(RES)/leader
|
|
||||||
./cutscc models/leader.ltl 4 models/leaderR.tgba > $(RES)/leaderR
|
|
||||||
./cutscc models/mobile1.ltl 4 models/mobile1.tgba > $(RES)/mobile1
|
|
||||||
./cutscc models/mobile1.ltl 4 models/mobile1R.tgba > $(RES)/mobile1R
|
|
||||||
./cutscc models/mobile2.ltl 4 models/mobile2.tgba > $(RES)/mobile2
|
|
||||||
./cutscc models/mobile2.ltl 4 models/mobile2R.tgba > $(RES)/mobile2R
|
|
||||||
./cutscc models/zune.ltl 4 models/zune.tgba > $(RES)/zune
|
|
||||||
./cutscc models/zune.ltl 4 models/zuneR.tgba > $(RES)/zuneR
|
|
||||||
|
|
@ -1,295 +0,0 @@
|
||||||
This directory contains the input files and test program used to produce
|
|
||||||
the measures for our new method consisting in splitting the automaton
|
|
||||||
corresponding to the formula in order to obtain smaller synchronised product.
|
|
||||||
This new method could lead to parallel computation of emptiness checks for
|
|
||||||
possibly faster results.
|
|
||||||
|
|
||||||
==========
|
|
||||||
CONTENTS
|
|
||||||
==========
|
|
||||||
|
|
||||||
This directory contains:
|
|
||||||
|
|
||||||
* models/cl3serv1.pml
|
|
||||||
* models/cl3serv3.pml
|
|
||||||
|
|
||||||
Two simple client/server promela examples.
|
|
||||||
|
|
||||||
* models/clserv.ltl
|
|
||||||
|
|
||||||
An LTL formula to verify on these examples.
|
|
||||||
|
|
||||||
* models/eeaean1.pml
|
|
||||||
* models/eeaean2.pml
|
|
||||||
|
|
||||||
Variations of the leader election protocol with extinction from
|
|
||||||
Tel, Introduction to Distributed Algorithms, 1994, Chapter 7. The
|
|
||||||
network in the model consists of three nodes. In Variant 1, the
|
|
||||||
same node wins every time, in Variant 2, each node gets a turn at
|
|
||||||
winning the election. These specifications were originally
|
|
||||||
distributed alongside
|
|
||||||
|
|
||||||
@InProceedings{ schwoon.05.tacas,
|
|
||||||
author = {Stefan Schwoon and Javier Esparza},
|
|
||||||
title = {A note on on-the-fly verification algorithms.},
|
|
||||||
booktitle = {Proceedings of the 11th International Conference
|
|
||||||
on Tools and Algorithms for the Construction and
|
|
||||||
Analysis of Systems
|
|
||||||
(TACAS'05)},
|
|
||||||
year = {2005},
|
|
||||||
series = {Lecture Notes in Computer Science},
|
|
||||||
publisher = {Springer-Verlag},
|
|
||||||
month = apr
|
|
||||||
}
|
|
||||||
|
|
||||||
* models/eeaean.ltl
|
|
||||||
|
|
||||||
Sample properties for the leader election protocols. These come from
|
|
||||||
|
|
||||||
@InProceedings{ geldenhuys.04.tacas,
|
|
||||||
author = {Jaco Geldenhuys and Antti Valmari},
|
|
||||||
title = {Tarjan's Algorithm Makes On-the-Fly {LTL} Verification
|
|
||||||
More Efficient},
|
|
||||||
booktitle = {Proceedings of the 10th International Conference on
|
|
||||||
Tools and Algorithms for the Construction and Analysis
|
|
||||||
of Systems
|
|
||||||
(TACAS'04)},
|
|
||||||
editor = {Kurt Jensen and Andreas Podelski},
|
|
||||||
pages = {205--219},
|
|
||||||
year = {2004},
|
|
||||||
publisher = {Springer-Verlag},
|
|
||||||
series = {Lecture Notes in Computer Science},
|
|
||||||
volume = {2988},
|
|
||||||
isbn = {3-540-21299-X}
|
|
||||||
}
|
|
||||||
|
|
||||||
* formulae.ltl
|
|
||||||
|
|
||||||
A list of 96 handwritten formulae with their negations. They come
|
|
||||||
from three sources:
|
|
||||||
|
|
||||||
@InProceedings{ dwyer.98.fmsp,
|
|
||||||
author = {Matthew B. Dwyer and George S. Avrunin and James C.
|
|
||||||
Corbett},
|
|
||||||
title = {Property Specification Patterns for Finite-state
|
|
||||||
Verification},
|
|
||||||
booktitle = {Proceedings of the 2nd Workshop on Formal Methods in
|
|
||||||
Software Practice (FMSP'98)},
|
|
||||||
publisher = {ACM Press},
|
|
||||||
address = {New York},
|
|
||||||
editor = {Mark Ardis},
|
|
||||||
month = mar,
|
|
||||||
year = {1998},
|
|
||||||
pages = {7--15}
|
|
||||||
}
|
|
||||||
|
|
||||||
@InProceedings{ etessami.00.concur,
|
|
||||||
author = {Kousha Etessami and Gerard J. Holzmann},
|
|
||||||
title = {Optimizing {B\"u}chi Automata},
|
|
||||||
booktitle = {Proceedings of the 11th International Conference on
|
|
||||||
Concurrency Theory (Concur'00)},
|
|
||||||
pages = {153--167},
|
|
||||||
year = {2000},
|
|
||||||
editor = {C. Palamidessi},
|
|
||||||
volume = {1877},
|
|
||||||
series = {Lecture Notes in Computer Science},
|
|
||||||
address = {Pennsylvania, USA},
|
|
||||||
publisher = {Springer-Verlag}
|
|
||||||
}
|
|
||||||
|
|
||||||
@InProceedings{ somenzi.00.cav,
|
|
||||||
author = {Fabio Somenzi and Roderick Bloem},
|
|
||||||
title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}},
|
|
||||||
booktitle = {Proceedings of the 12th International Conference on
|
|
||||||
Computer Aided Verification (CAV'00)},
|
|
||||||
pages = {247--263},
|
|
||||||
year = {2000},
|
|
||||||
volume = {1855},
|
|
||||||
series = {Lecture Notes in Computer Science},
|
|
||||||
address = {Chicago, Illinois, USA},
|
|
||||||
publisher = {Springer-Verlag}
|
|
||||||
}
|
|
||||||
|
|
||||||
* models/mobile1.pml
|
|
||||||
|
|
||||||
File found in /Spin/Test/
|
|
||||||
Model of cell-phone handoff strategy in a mobile network.
|
|
||||||
A translation from the pi-calculus description of this model presented in:
|
|
||||||
|
|
||||||
@ARTICLE{ Orava91analgebraic,
|
|
||||||
author = {Fredrik Orava and Joachim Parrow},
|
|
||||||
title = {An Algebraic Verification of a Mobile Network},
|
|
||||||
journal = {Formal Aspects of Computing},
|
|
||||||
year = {1991},
|
|
||||||
volume = {4},
|
|
||||||
pages = {497--543}
|
|
||||||
}
|
|
||||||
|
|
||||||
* models/mobile2.pml
|
|
||||||
|
|
||||||
File found in /Spin/Test/
|
|
||||||
Simplified model of cell-phone handoff strategy in a mobile network.
|
|
||||||
A translation from the pi-calculus description of this model presented in
|
|
||||||
the same article as above.
|
|
||||||
|
|
||||||
* models/leader.pml
|
|
||||||
|
|
||||||
File found in /Spin/Test/
|
|
||||||
O(n log n) algorithm for leader election in unidirectional ring.
|
|
||||||
Presented in:
|
|
||||||
|
|
||||||
@InProceedings{Afek97self-stabilizingunidirectional,
|
|
||||||
author = {Yehuda Afek and Anat Bremler},
|
|
||||||
title = {Self-Stabilizing Unidirectional Network Algorithms
|
|
||||||
by Power-Supply},
|
|
||||||
booktitle = {Chicago Journal of Theoretical Computer Science},
|
|
||||||
year = {1997},
|
|
||||||
pages = {111--120},
|
|
||||||
publisher = {The MIT Press}
|
|
||||||
}
|
|
||||||
|
|
||||||
* models/zune.pml
|
|
||||||
|
|
||||||
File found in Spin/Test/
|
|
||||||
A bug caused all Zune-30 players to freeze on Dec 31, 2008
|
|
||||||
http://www.zuneboards.com/forums/zune-news/38143-cause-zune-30-leapyear-problem-isolated.html
|
|
||||||
The bug was in the firmware clock-driver, which was written by Freescale
|
|
||||||
for their MC13783 PMIC processor.
|
|
||||||
input: days elapsed since Jan 1, 1980
|
|
||||||
intended output: year and daynr in current year
|
|
||||||
|
|
||||||
* models/cl3serv1.tgba
|
|
||||||
* models/cl3serv3.tgba
|
|
||||||
* models/cl3serv1R.tgba
|
|
||||||
* models/cl3serv3R.tgba
|
|
||||||
* models/eeaean1.tgba (12MB)
|
|
||||||
* models/eeaean2.tgba (38MB)
|
|
||||||
* models/eeaean1R.tgba
|
|
||||||
* models/eeaean2R.tgba
|
|
||||||
* models/leader.tgba
|
|
||||||
* models/leaderR.tgba
|
|
||||||
* models/mobile1.tgba
|
|
||||||
* models/mobile1R.tgba
|
|
||||||
* models/mobile2.tgba
|
|
||||||
* models/mobile2R.tgba
|
|
||||||
* models/zune.tgba
|
|
||||||
* models/zumeR.tgba
|
|
||||||
|
|
||||||
The corresponding TGBA for the Promela models introduced above.
|
|
||||||
They were translated by pml2tgba.pl (located in bench/emptchk/)
|
|
||||||
into an input format readable by SPOT.
|
|
||||||
Promela inputs can be translated in 4 different graphs.
|
|
||||||
For instance eeaean1.pml is translated as
|
|
||||||
- eeaean1.tgba full translation
|
|
||||||
- eeaean1R.tgba reduced translation
|
|
||||||
The "reduced" translation uses Spin's partial order reductions.
|
|
||||||
|
|
||||||
* results/<model_name>
|
|
||||||
|
|
||||||
For each <model_name>.tgba model in models you can find a simple text file
|
|
||||||
named <model_name>.
|
|
||||||
Each file present the results of our own benchmarks.
|
|
||||||
See the INTERPRETING RESULTS section for further details.
|
|
||||||
|
|
||||||
=======
|
|
||||||
USAGE
|
|
||||||
=======
|
|
||||||
|
|
||||||
Use the cutscc program.
|
|
||||||
Usage: ./cutscc ltl_formulae split_number [model]
|
|
||||||
Where
|
|
||||||
- ltl_formulae is a ltl file with one formula per line.
|
|
||||||
- split_number is the maximum number of sub automata after splitting.
|
|
||||||
Remember this is a maximum value, the effective splitting can be between
|
|
||||||
1 and split_number automata.
|
|
||||||
- model is the .tgba input file translated from Promela for Spot.
|
|
||||||
If no model is speficied, a random graph with 10 000 nodes will be
|
|
||||||
generated.
|
|
||||||
|
|
||||||
Sample examples :
|
|
||||||
./cutscc models/eeaean.ltl 2 models/eeaean1.tgba
|
|
||||||
./cutscc models/formulae.ltl 2
|
|
||||||
|
|
||||||
==========================
|
|
||||||
INTERPRETING THE RESULTS
|
|
||||||
==========================
|
|
||||||
|
|
||||||
By default, all results are printed on standard output. Redirect them
|
|
||||||
with ">" to erase files in cut-results/ or to create new benchs files.
|
|
||||||
|
|
||||||
The output looks as follow, first, the global header:
|
|
||||||
| Reference automaton has 49332 states.
|
|
||||||
| Trying to split each automaton in 9 sub automata.
|
|
||||||
| Each operation is repeated 100 times to improve precision.
|
|
||||||
First, if we specified a single model, we have the size of our model.
|
|
||||||
The second line is a recall of split_number value.
|
|
||||||
The third line is the number of iteration repeated to increase the precision
|
|
||||||
of benchmarks for each key operation. It greatly slows down the whole process.
|
|
||||||
To measure the elapsed time we simply compute the difference between
|
|
||||||
gettimeofday() before and after our operation.
|
|
||||||
|
|
||||||
For each formula, the result looks as follow :
|
|
||||||
| Formula 9
|
|
||||||
| !((<>[](noLeader || zeroLeads || oneLeads || twoLeads)) && (<>[]((zeroLeads -> (zeroLeads U (noLeader U twoLeads))))) && (<>[]((oneLeads -> (oneLeads U (noLeader U zeroLeads))))) && (<>[]((twoLeads -> (twoLeads U (noLeader U oneLeads))))))
|
|
||||||
|
|
|
||||||
First, the number of the formula, i.e the corresponding line in the ltl file.
|
|
||||||
On the following line the formula is recalled
|
|
||||||
|
|
||||||
| Full Product : 247864 states in 0.002611s
|
|
||||||
| 361 unique states visited
|
|
||||||
| 27 strongly connected components in search stack
|
|
||||||
| 412 transitions explored
|
|
||||||
| 361 items max in DFS search stack
|
|
||||||
|
|
|
||||||
Stats of the synchronised product and emptiness check computed on the main
|
|
||||||
unsplitted automaton.
|
|
||||||
|
|
||||||
| Splitting in 0.000212s
|
|
||||||
| Base automaton splitted in 4 automata.
|
|
||||||
|
|
|
||||||
Details about splitting time and number of sub automata created.
|
|
||||||
Here, we wished every formula would have been splitted in 9, but here
|
|
||||||
it could only be splitted in 4.
|
|
||||||
|
|
||||||
| Product 1 : 99871 states in 0.002614s
|
|
||||||
| 361 unique states visited
|
|
||||||
| 27 strongly connected components in search stack
|
|
||||||
| 412 transitions explored
|
|
||||||
| 361 items max in DFS search stack
|
|
||||||
|
|
|
||||||
| Product 2 : 49332 states in 0.297583s
|
|
||||||
| No accepting path.
|
|
||||||
|
|
|
||||||
| Product 3 : 49332 states in 0.297967s
|
|
||||||
| No accepting path.
|
|
||||||
|
|
|
||||||
| Product 4 : 49332 states in 0.296978s
|
|
||||||
| No accepting path.
|
|
||||||
|
|
|
||||||
Details concerning synchronised product size and emptiness check on each
|
|
||||||
sub automaton, in the same format as above for the full formula.
|
|
||||||
|
|
||||||
| Total split products size : 247867
|
|
||||||
| Additionnal states created : 3
|
|
||||||
| Additionnal states ratio : 0.000012
|
|
||||||
| Cutting and computing time : 0.002826s
|
|
||||||
| Time gain -0.000214s
|
|
||||||
Overall data for this formula, we compute the size of our splitted
|
|
||||||
synchronised products by simply adding them. This is an important
|
|
||||||
factor because sometimes an excessively large number of states are generated
|
|
||||||
with this method compared to the original product.
|
|
||||||
The two last lines give the speed results of splitting and computing emptiness
|
|
||||||
check on the sub automata.
|
|
||||||
If there is an accepting path, we take the shortest time because it means an
|
|
||||||
early stop in our algorithm, we can stop computation for other sub automata.
|
|
||||||
If there are no accepting path, we take the longest time because it means a
|
|
||||||
mandatory full traversal of all automaton.
|
|
||||||
|
|
||||||
At the end we sum the computation times for the full formula and the splitted
|
|
||||||
formula:
|
|
||||||
| Full 3.145159s
|
|
||||||
| Cutting 0.000212s
|
|
||||||
| Split 2.522595s
|
|
||||||
This is more or less significant, sometime splitting will greatly improve
|
|
||||||
speed for a single formula and will have small or no impact on others.
|
|
||||||
|
|
||||||
|
|
@ -1,343 +0,0 @@
|
||||||
// -*- coding: utf-8 -*-
|
|
||||||
// Copyright (C) 2009, 2010, 2012, 2013 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/>.
|
|
||||||
|
|
||||||
#include <queue>
|
|
||||||
#include <limits>
|
|
||||||
#include <sys/time.h>
|
|
||||||
#include "tgbaalgos/scc.hh"
|
|
||||||
#include "ltlparse/ltlfile.hh"
|
|
||||||
#include "ltlvisit/tostring.hh"
|
|
||||||
#include "tgbaalgos/dotty.hh"
|
|
||||||
#include "tgbaalgos/randomgraph.hh"
|
|
||||||
#include "tgbaalgos/emptiness.hh"
|
|
||||||
#include "tgba/tgbaproduct.hh"
|
|
||||||
#include "tgbaalgos/replayrun.hh"
|
|
||||||
#include "tgbaalgos/emptiness_stats.hh"
|
|
||||||
#include "ltlvisit/apcollect.hh"
|
|
||||||
#include "tgbaparse/public.hh"
|
|
||||||
#include "tgbaalgos/cutscc.hh"
|
|
||||||
#include "tgbaalgos/ltl2tgba_fm.hh"
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
unsigned tgba_size(const tgba* a)
|
|
||||||
{
|
|
||||||
typedef std::unordered_set<const state*,
|
|
||||||
state_ptr_hash, state_ptr_equal> hash_type;
|
|
||||||
hash_type seen;
|
|
||||||
std::queue<state*> tovisit;
|
|
||||||
// Perform breadth-first search.
|
|
||||||
state* init = a->get_init_state();
|
|
||||||
tovisit.push(init);
|
|
||||||
seen.insert(init);
|
|
||||||
unsigned count = 0;
|
|
||||||
// While there are still states to visit.
|
|
||||||
while (!tovisit.empty())
|
|
||||||
{
|
|
||||||
++count;
|
|
||||||
state* cur = tovisit.front();
|
|
||||||
tovisit.pop();
|
|
||||||
tgba_succ_iterator* sit = a->succ_iter(cur);
|
|
||||||
for (sit->first(); !sit->done(); sit->next())
|
|
||||||
{
|
|
||||||
state* dst = sit->current_state();
|
|
||||||
// Is it a new state ?
|
|
||||||
if (seen.find(dst) == seen.end())
|
|
||||||
{
|
|
||||||
// Yes, register the successor for later processing.
|
|
||||||
tovisit.push(dst);
|
|
||||||
seen.insert(dst);
|
|
||||||
}
|
|
||||||
else
|
|
||||||
// No, free dst.
|
|
||||||
dst->destroy();
|
|
||||||
}
|
|
||||||
delete sit;
|
|
||||||
}
|
|
||||||
hash_type::iterator it2;
|
|
||||||
// Free visited states.
|
|
||||||
for (it2 = seen.begin(); it2 != seen.end(); it2++)
|
|
||||||
(*it2)->destroy();
|
|
||||||
return count;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
void TimerReset(struct timeval& start)
|
|
||||||
{
|
|
||||||
// Initialize timer with the current time.
|
|
||||||
gettimeofday(&start, 0);
|
|
||||||
}
|
|
||||||
|
|
||||||
double TimerGetElapsedTime(struct timeval& start)
|
|
||||||
{
|
|
||||||
// Compute the diferrence between now and the time when start was initialized.
|
|
||||||
double t1, t2;
|
|
||||||
struct timeval end;
|
|
||||||
TimerReset(end);
|
|
||||||
t1 = (double)start.tv_sec + (double)start.tv_usec*0.000001;
|
|
||||||
t2 = (double)end.tv_sec + (double)end.tv_usec*0.000001;
|
|
||||||
|
|
||||||
return t2 - t1;
|
|
||||||
}
|
|
||||||
|
|
||||||
bool accepting_path(spot::tgba* a, std::ostream& output, bool do_print)
|
|
||||||
{
|
|
||||||
const char* err;
|
|
||||||
spot::emptiness_check_instantiator* inst;
|
|
||||||
inst = spot::emptiness_check_instantiator::construct("Cou99", &err);
|
|
||||||
spot::emptiness_check* ec = inst->instantiate(a);
|
|
||||||
spot::emptiness_check_result* acc;
|
|
||||||
acc = ec->check();
|
|
||||||
spot::tgba_run* run;
|
|
||||||
|
|
||||||
if (acc)
|
|
||||||
{
|
|
||||||
run = acc->accepting_run();
|
|
||||||
//const spot::unsigned_statistics* stats = acc->statistics();
|
|
||||||
//spot::Replay_tgba_run(output, acc->automaton(), run);
|
|
||||||
if (do_print)
|
|
||||||
ec->print_stats(output);
|
|
||||||
delete run;
|
|
||||||
delete acc;
|
|
||||||
}
|
|
||||||
else if (do_print)
|
|
||||||
std::cout << "No accepting path." << std::endl;
|
|
||||||
delete inst;
|
|
||||||
delete ec;
|
|
||||||
return acc != 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
int main(int argc, char* argv[])
|
|
||||||
{
|
|
||||||
if (argc > 4)
|
|
||||||
{
|
|
||||||
std::cout << "Usage ./cutscc file_name split_count [model_file]"
|
|
||||||
<< std::endl;
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
std::ofstream out_dot ("auto.dot");
|
|
||||||
std::cout.setf (std::ios::fixed);
|
|
||||||
bool print_size = true;
|
|
||||||
bool print_time = true;
|
|
||||||
bool print_ec = true;
|
|
||||||
int i = 0;
|
|
||||||
int split_count = atoi(argv[2]);
|
|
||||||
std::vector<bool> accepting_vector;
|
|
||||||
accepting_vector.reserve(10000);
|
|
||||||
double split_sum = 0.;
|
|
||||||
double full_sum = 0.;
|
|
||||||
double cut_sum = 0.;
|
|
||||||
spot::tgba* r = 0;
|
|
||||||
spot::ltl::environment& env(spot::ltl::default_environment::instance());
|
|
||||||
spot::bdd_dict* dict = new spot::bdd_dict();
|
|
||||||
if (argc == 4)
|
|
||||||
{
|
|
||||||
spot::tgba_parse_error_list error_list;
|
|
||||||
r = spot::tgba_parse(argv[3], error_list, dict, env, env, false);
|
|
||||||
if (print_size)
|
|
||||||
std::cout << "Reference automaton has " << tgba_size(r)
|
|
||||||
<< " states." << std::endl
|
|
||||||
<<"Trying to split each automaton in " << split_count
|
|
||||||
<< " sub automata." << std::endl;
|
|
||||||
}
|
|
||||||
// iter_count is the number of iterations done to increase precision.
|
|
||||||
unsigned iter_count = 1;
|
|
||||||
std::cout << "Each operation is repeated " << iter_count
|
|
||||||
<< " times to improve precision." << std::endl << std::endl;
|
|
||||||
|
|
||||||
spot::ltl::ltl_file formulae(argv[1]);
|
|
||||||
while (const spot::ltl::formula* f = formulae.next())
|
|
||||||
{
|
|
||||||
spot::tgba* a = ltl_to_tgba_fm(f, dict, /* exprop */ true);
|
|
||||||
++i;
|
|
||||||
std::cout << "Formula " << i << std::endl;
|
|
||||||
std::cout << spot::ltl::to_string(f) << std::endl << std::endl;
|
|
||||||
if (argc != 4)
|
|
||||||
{
|
|
||||||
spot::ltl::atomic_prop_set* s;
|
|
||||||
s = spot::ltl::atomic_prop_collect(f, 0);
|
|
||||||
spot::ltl::atomic_prop_set::iterator sit;
|
|
||||||
delete r;
|
|
||||||
r = spot::random_graph(10000, 0.0001, s, dict, 0, 0.15, 0.5);
|
|
||||||
delete s;
|
|
||||||
}
|
|
||||||
spot::scc_map m (a);
|
|
||||||
m.build_map();
|
|
||||||
|
|
||||||
spot::tgba* res = 0;
|
|
||||||
|
|
||||||
// Simplify the tgba to delete useless pathes
|
|
||||||
if (argc != 4)
|
|
||||||
{
|
|
||||||
spot::tgba* tmp = a;
|
|
||||||
a = spot::split_tgba(a, m, 1).front();
|
|
||||||
delete tmp;
|
|
||||||
}
|
|
||||||
|
|
||||||
struct timeval start;
|
|
||||||
double elapsed = 0.;
|
|
||||||
bool full_result;
|
|
||||||
unsigned j;
|
|
||||||
for (j = 0; j < iter_count; j++)
|
|
||||||
{
|
|
||||||
// Measure the mean computing time for the product with our full
|
|
||||||
// automaton.
|
|
||||||
TimerReset(start);
|
|
||||||
res = new spot::tgba_product(r, a);
|
|
||||||
full_result = accepting_path(res, std::cout, false);
|
|
||||||
elapsed += TimerGetElapsedTime(start);
|
|
||||||
delete res;
|
|
||||||
}
|
|
||||||
double full_time = elapsed / iter_count;
|
|
||||||
full_sum += full_time;
|
|
||||||
// Compute again for printing purposes only.
|
|
||||||
res = new spot::tgba_product(r, a);
|
|
||||||
|
|
||||||
unsigned full_size;
|
|
||||||
if (print_size)
|
|
||||||
{
|
|
||||||
full_size = tgba_size(res);
|
|
||||||
std::cout << "Full Product : " << full_size << " states";
|
|
||||||
}
|
|
||||||
if (print_time)
|
|
||||||
{
|
|
||||||
std::cout << " in " << elapsed / iter_count << "s";
|
|
||||||
}
|
|
||||||
std::cout << std::endl;
|
|
||||||
if (print_ec)
|
|
||||||
{
|
|
||||||
accepting_path(res, std::cout, true);
|
|
||||||
std::cout << std::endl;
|
|
||||||
}
|
|
||||||
delete res;
|
|
||||||
|
|
||||||
double cut_time = 0.;
|
|
||||||
std::list<spot::tgba*> splitted;
|
|
||||||
for (j = 0; j < iter_count; j++)
|
|
||||||
{
|
|
||||||
// Mean computing time to split the automaton in split_count automata
|
|
||||||
spot::scc_map m2 (a);
|
|
||||||
m2.build_map();
|
|
||||||
TimerReset(start);
|
|
||||||
splitted = spot::split_tgba(a, m2, split_count);
|
|
||||||
cut_time += TimerGetElapsedTime(start);
|
|
||||||
std::list<spot::tgba*>::iterator lit;
|
|
||||||
for (lit = splitted.begin(); lit != splitted.end(); lit++)
|
|
||||||
delete *lit;
|
|
||||||
}
|
|
||||||
|
|
||||||
cut_sum = cut_time / iter_count;
|
|
||||||
// Compute again for printing purposes only
|
|
||||||
spot::scc_map m2 (a);
|
|
||||||
m2.build_map();
|
|
||||||
// if (i == 42)
|
|
||||||
// spot::dotty_reachable(out_dot, a);
|
|
||||||
splitted = spot::split_tgba(a, m2, split_count);
|
|
||||||
if (print_time)
|
|
||||||
{
|
|
||||||
std::cout << "Splitting in "
|
|
||||||
<< cut_time / iter_count << "s" << std::endl;
|
|
||||||
}
|
|
||||||
|
|
||||||
double min = std::numeric_limits<double>::max();
|
|
||||||
double max = 0.;
|
|
||||||
accepting_vector[i] = false;
|
|
||||||
unsigned split_size = 0;
|
|
||||||
if (print_size)
|
|
||||||
std::cout << "Base automaton splitted in " << splitted.size()
|
|
||||||
<< " automata." << std::endl;
|
|
||||||
std::cout << std::endl;
|
|
||||||
unsigned k = 1;
|
|
||||||
std::list<spot::tgba*>::iterator it;
|
|
||||||
for (it = splitted.begin(); it != splitted.end(); ++it)
|
|
||||||
{
|
|
||||||
elapsed = 0;
|
|
||||||
for (j = 0; j < iter_count; j++)
|
|
||||||
{
|
|
||||||
// Compute mean computing time for the product with only a part of the
|
|
||||||
// full automaton.
|
|
||||||
TimerReset(start);
|
|
||||||
res = new spot::tgba_product(r, *it);
|
|
||||||
bool is_accepting = accepting_path(res, std::cout, false);
|
|
||||||
accepting_vector[i] = accepting_vector[i]
|
|
||||||
|| is_accepting;
|
|
||||||
elapsed += TimerGetElapsedTime(start);
|
|
||||||
delete res;
|
|
||||||
}
|
|
||||||
res = new spot::tgba_product(r, *it);
|
|
||||||
elapsed = elapsed / iter_count;
|
|
||||||
if (print_size)
|
|
||||||
{
|
|
||||||
unsigned size = tgba_size(res);
|
|
||||||
split_size += size;
|
|
||||||
std::cout << "Product " << k << " : " << size
|
|
||||||
<< " states in " << elapsed << "s" << std::endl;
|
|
||||||
}
|
|
||||||
bool is_accepting;
|
|
||||||
if (print_ec)
|
|
||||||
{
|
|
||||||
is_accepting = accepting_path(res, std::cout, true);
|
|
||||||
std::cout << std::endl;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
is_accepting = accepting_path(res, std::cout, false);
|
|
||||||
++k;
|
|
||||||
|
|
||||||
delete res;
|
|
||||||
if (is_accepting)
|
|
||||||
min = (elapsed<min) ? elapsed:min;
|
|
||||||
else
|
|
||||||
max = (elapsed>max) ? elapsed:max;
|
|
||||||
}
|
|
||||||
if (print_size)
|
|
||||||
{
|
|
||||||
std::cout << "Total split products size : " << split_size << std::endl;
|
|
||||||
unsigned added_states = 0.;
|
|
||||||
added_states = split_size - full_size;
|
|
||||||
double time_gain = full_time -
|
|
||||||
(((accepting_vector[i]) ? min:max) + (cut_time / iter_count));
|
|
||||||
std::cout << "Additionnal states created : " << added_states
|
|
||||||
<< std::endl;
|
|
||||||
std::cout << "Additionnal states ratio : "
|
|
||||||
<< double(added_states) / full_size << std::endl;
|
|
||||||
std::cout << "Cutting and computing time : "
|
|
||||||
<< ((accepting_vector[i]) ? min:max) + (cut_time / iter_count)
|
|
||||||
<< "s" << std::endl;
|
|
||||||
std::cout << "Time gain " << time_gain << "s" << std::endl;
|
|
||||||
std::cout << std::endl;
|
|
||||||
}
|
|
||||||
std::list<spot::tgba*>::iterator lit;
|
|
||||||
for (lit = splitted.begin(); lit != splitted.end(); lit++)
|
|
||||||
delete *lit;
|
|
||||||
if (accepting_vector[i] != full_result)
|
|
||||||
std::cout << "Disagree !" << std::endl;
|
|
||||||
split_sum += (accepting_vector[i]) ? min:max;
|
|
||||||
|
|
||||||
delete a;
|
|
||||||
f->destroy();
|
|
||||||
std::string next = "----------------------------------------";
|
|
||||||
std::cout << next << next << std::endl;
|
|
||||||
std::cout << std::endl;
|
|
||||||
}
|
|
||||||
delete r;
|
|
||||||
delete dict;
|
|
||||||
std::cout << "Full " << full_sum << "s" << std::endl
|
|
||||||
<< "Cutting " << cut_sum << "s" << std::endl
|
|
||||||
<< "Split " << split_sum << "s" << std::endl;
|
|
||||||
}
|
|
||||||
|
|
@ -1,55 +0,0 @@
|
||||||
[](!p0)
|
|
||||||
<>p1 -> (!p0 U p1)
|
|
||||||
[](p2 -> [](!p0))
|
|
||||||
[]((p2 & !p1 & <>p1) -> (!p0 U p1))
|
|
||||||
[](p2 & !p1 -> (!p0 U (p1 | []!p0)))
|
|
||||||
<>(p0)
|
|
||||||
!p1 U ((p0 & !p1) | []!p1)
|
|
||||||
[](!p2) | <>(p2 & <>p0)
|
|
||||||
[](p2 & !p1 -> (!p1 U ((p0 & !p1) | []!p1)))
|
|
||||||
[](p2 & !p1 -> (!p1 U (p0 & !p1)))
|
|
||||||
<>p1 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1)))))))))
|
|
||||||
[]((p2 & <>p1) -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1))))))))))
|
|
||||||
[](p2 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U (p1 | []!p0)) | []p0)))))))))
|
|
||||||
[](p0)
|
|
||||||
<>p1 -> (p0 U p1)
|
|
||||||
[](p2 -> [](p0))
|
|
||||||
[]((p2 & !p1 & <>p1) -> (p0 U p1))
|
|
||||||
[](p2 & !p1 -> (p0 U (p1 | [] p0)))
|
|
||||||
!p0 U (p3 | []!p0)
|
|
||||||
<>p1 -> (!p0 U (p3 | p1))
|
|
||||||
[]!p2 | <>(p2 & (!p0 U (p3 | []!p0)))
|
|
||||||
[]((p2 & !p1 & <>p1) -> (!p0 U (p3 | p1)))
|
|
||||||
[](p2 & !p1 -> (!p0 U ((p3 | p1) | []!p0)))
|
|
||||||
[](p0 -> <>p3)
|
|
||||||
<>p1 -> (p0 -> (!p1 U (p3 & !p1))) U p1
|
|
||||||
[](p2 -> [](p0 -> <>p3))
|
|
||||||
[]((p2 & !p1 & <>p1) -> (p0 -> (!p1 U (p3 & !p1))) U p1)
|
|
||||||
[](p2 & !p1 -> ((p0 -> (!p1 U (p3 & !p1))) U (p1 | [](p0 -> (!p1 U (p3 & !p1))))))
|
|
||||||
<>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))
|
|
||||||
<>p1 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))
|
|
||||||
([]!p2) | (!p2 U (p2 & <>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))))
|
|
||||||
[]((p2 & <>p1) -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4)))))
|
|
||||||
[](p2 -> (<>p0 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))))
|
|
||||||
(<>(p3 & X<>p4)) -> ((!p3) U p0)
|
|
||||||
<>p1 -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0))
|
|
||||||
([]!p2) | ((!p2) U (p2 & ((<>(p3 & X<>p4)) -> ((!p3) U p0))))
|
|
||||||
[]((p2 & <>p1) -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0)))
|
|
||||||
[](p2 -> (!(p3 & (!p1) & X(!p1 U (p4 & !p1))) U (p1 | p0) | [](!(p3 & X<>p4))))
|
|
||||||
[] (p3 & X<> p4 -> X(<>(p4 & <> p0)))
|
|
||||||
<>p1 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1
|
|
||||||
[] (p2 -> [] (p3 & X<> p4 -> X(!p4 U (p4 & <> p0))))
|
|
||||||
[] ((p2 & <>p1) -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1)
|
|
||||||
[] (p2 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U (p1 | [] (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0)))))
|
|
||||||
[] (p0 -> <>(p3 & X<>p4))
|
|
||||||
<>p1 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1
|
|
||||||
[] (p2 -> [] (p0 -> (p3 & X<> p4)))
|
|
||||||
[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1)
|
|
||||||
[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U (p1 | [] (p0 -> (p3 & X<> p4))))
|
|
||||||
[] (p0 -> <>(p3 & !p5 & X(!p5 U p4)))
|
|
||||||
<>p1 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1
|
|
||||||
[] (p2 -> [] (p0 -> (p3 & !p5 & X(!p5 U p4))))
|
|
||||||
[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1)
|
|
||||||
[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U (p1 | [] (p0 -> (p3 & !p5 & X(!p5 U p4)))))
|
|
||||||
!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0)
|
|
||||||
<>p2 -> (!p2 U (p2 & (!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0))))
|
|
||||||
|
|
@ -1,43 +0,0 @@
|
||||||
#define w1 client[0]@wait
|
|
||||||
#define s1 client[0]@served
|
|
||||||
|
|
||||||
#define C 3
|
|
||||||
#define S 1
|
|
||||||
|
|
||||||
chan clserv = [C] of { int };
|
|
||||||
chan servcl = [S] of { int };
|
|
||||||
|
|
||||||
active [C] proctype client() {
|
|
||||||
/* the _pid's are: 0 .. C-1 */
|
|
||||||
|
|
||||||
served:
|
|
||||||
if
|
|
||||||
:: (1) -> goto request;
|
|
||||||
fi;
|
|
||||||
request:
|
|
||||||
if
|
|
||||||
:: (1) -> clserv!_pid; goto wait;
|
|
||||||
fi;
|
|
||||||
wait:
|
|
||||||
if
|
|
||||||
:: servcl?eval(_pid); goto served;
|
|
||||||
fi;
|
|
||||||
}
|
|
||||||
|
|
||||||
active [S] proctype server() {
|
|
||||||
/* the _pid's are: 0 .. S-1 */
|
|
||||||
byte id;
|
|
||||||
|
|
||||||
wait:
|
|
||||||
if
|
|
||||||
:: clserv?id -> goto work;
|
|
||||||
fi;
|
|
||||||
work:
|
|
||||||
if
|
|
||||||
:: (1) -> goto reply;
|
|
||||||
fi;
|
|
||||||
reply:
|
|
||||||
if
|
|
||||||
:: (1) -> servcl!id; goto wait;
|
|
||||||
fi;
|
|
||||||
}
|
|
||||||
|
|
@ -1,43 +0,0 @@
|
||||||
#define w1 client[0]@wait
|
|
||||||
#define s1 client[0]@served
|
|
||||||
|
|
||||||
#define C 3
|
|
||||||
#define S 3
|
|
||||||
|
|
||||||
chan clserv = [C] of { int };
|
|
||||||
chan servcl = [S] of { int };
|
|
||||||
|
|
||||||
active [C] proctype client() {
|
|
||||||
/* the _pid's are: 0 .. C-1 */
|
|
||||||
|
|
||||||
served:
|
|
||||||
if
|
|
||||||
:: (1) -> goto request;
|
|
||||||
fi;
|
|
||||||
request:
|
|
||||||
if
|
|
||||||
:: (1) -> clserv!_pid; goto wait;
|
|
||||||
fi;
|
|
||||||
wait:
|
|
||||||
if
|
|
||||||
:: servcl?eval(_pid); goto served;
|
|
||||||
fi;
|
|
||||||
}
|
|
||||||
|
|
||||||
active [S] proctype server() {
|
|
||||||
/* the _pid's are: 0 .. S-1 */
|
|
||||||
byte id;
|
|
||||||
|
|
||||||
wait:
|
|
||||||
if
|
|
||||||
:: clserv?id -> goto work;
|
|
||||||
fi;
|
|
||||||
work:
|
|
||||||
if
|
|
||||||
:: (1) -> goto reply;
|
|
||||||
fi;
|
|
||||||
reply:
|
|
||||||
if
|
|
||||||
:: (1) -> servcl!id; goto wait;
|
|
||||||
fi;
|
|
||||||
}
|
|
||||||
|
|
@ -1 +0,0 @@
|
||||||
!([] (w1 -> <> s1))
|
|
||||||
|
|
@ -1,9 +0,0 @@
|
||||||
!(<>[](noLeader U zeroLeads))
|
|
||||||
!(<>[](noLeader U threeLeads))
|
|
||||||
!(<>zeroLeads)
|
|
||||||
!([]<>zeroLeads)
|
|
||||||
!(<>threeLeads)
|
|
||||||
!([](noLeader -> <>zeroLeads))
|
|
||||||
!([](noLeader || zeroLeads))
|
|
||||||
!((<>[](noLeader || zeroLeads || oneLeads || twoLeads)) && (<>[]((zeroLeads -> (zeroLeads U (noLeader U oneLeads))))) && (<>[]((oneLeads -> (oneLeads U (noLeader U twoLeads))))) && (<>[]((twoLeads -> (twoLeads U (noLeader U zeroLeads))))))
|
|
||||||
!((<>[](noLeader || zeroLeads || oneLeads || twoLeads)) && (<>[]((zeroLeads -> (zeroLeads U (noLeader U twoLeads))))) && (<>[]((oneLeads -> (oneLeads U (noLeader U zeroLeads))))) && (<>[]((twoLeads -> (twoLeads U (noLeader U oneLeads))))))
|
|
||||||
|
|
@ -1,116 +0,0 @@
|
||||||
/* Echo Election Algorithm with Extinction in an Arbitrary Network. */
|
|
||||||
/* Variation 1: Node 0 wins every time. */
|
|
||||||
|
|
||||||
#define L 10 /* size of buffer */
|
|
||||||
#define udef 3
|
|
||||||
|
|
||||||
#define noLeader (nr_leaders == 0)
|
|
||||||
#define zeroLeads (nr_leaders == 1 && leader == 0)
|
|
||||||
#define oneLeads (nr_leaders == 1 && leader == 1)
|
|
||||||
#define twoLeads (nr_leaders == 1 && leader == 2)
|
|
||||||
#define threeLeads (nr_leaders == 1 && leader == 3)
|
|
||||||
|
|
||||||
mtype = { tok, ldr };
|
|
||||||
chan zero_one = [L] of { mtype, byte};
|
|
||||||
chan zero_two = [L] of { mtype, byte};
|
|
||||||
chan one_zero = [L] of { mtype, byte};
|
|
||||||
chan one_two = [L] of { mtype, byte};
|
|
||||||
chan two_zero = [L] of { mtype, byte};
|
|
||||||
chan two_one = [L] of { mtype, byte};
|
|
||||||
|
|
||||||
chan nr0 = [0] of {mtype};
|
|
||||||
chan nr1 = [0] of {mtype};
|
|
||||||
chan nr2 = [0] of {mtype};
|
|
||||||
|
|
||||||
byte nr_leaders, done, leader;
|
|
||||||
|
|
||||||
inline recvldr ()
|
|
||||||
{
|
|
||||||
if
|
|
||||||
:: lrec == 0 && r != myid ->
|
|
||||||
out1!ldr(r);
|
|
||||||
out2!ldr(r);
|
|
||||||
:: else -> skip;
|
|
||||||
fi;
|
|
||||||
lrec++;
|
|
||||||
win = r;
|
|
||||||
}
|
|
||||||
|
|
||||||
inline recvtok (q,c)
|
|
||||||
{
|
|
||||||
if
|
|
||||||
:: r < caw ->
|
|
||||||
caw = r;
|
|
||||||
rec = 0;
|
|
||||||
father = q;
|
|
||||||
c!tok(r);
|
|
||||||
:: else -> skip;
|
|
||||||
fi;
|
|
||||||
|
|
||||||
if
|
|
||||||
:: r == caw ->
|
|
||||||
rec++;
|
|
||||||
if
|
|
||||||
:: rec == 2 && caw == myid
|
|
||||||
-> out1!ldr(myid); out2!ldr(myid);
|
|
||||||
:: rec == 2 && caw != myid && father == neigh1
|
|
||||||
-> out1!tok(caw)
|
|
||||||
:: rec == 2 && caw != myid && father == neigh2
|
|
||||||
-> out2!tok(caw)
|
|
||||||
:: else -> skip;
|
|
||||||
fi;
|
|
||||||
:: else -> skip;
|
|
||||||
fi;
|
|
||||||
}
|
|
||||||
|
|
||||||
proctype node (chan nr; byte neigh1; chan out1, in1;
|
|
||||||
byte neigh2; chan out2, in2)
|
|
||||||
{ byte myid = 3 - neigh1 - neigh2;
|
|
||||||
byte caw, rec, father, lrec, win, r;
|
|
||||||
|
|
||||||
xr in1; xr in2;
|
|
||||||
xs out1; xs out2;
|
|
||||||
|
|
||||||
restart:
|
|
||||||
nr?tok;
|
|
||||||
caw = myid; rec = 0; lrec = 0;
|
|
||||||
father = udef; win = udef; r = udef;
|
|
||||||
|
|
||||||
out1!tok(myid);
|
|
||||||
out2!tok(myid);
|
|
||||||
do
|
|
||||||
:: lrec == 2 -> break;
|
|
||||||
:: in1?ldr(r) -> recvldr();
|
|
||||||
:: in2?ldr(r) -> recvldr();
|
|
||||||
:: in1?tok(r) -> recvtok(neigh1,out2);
|
|
||||||
:: in2?tok(r) -> recvtok(neigh2,out1);
|
|
||||||
od;
|
|
||||||
|
|
||||||
if
|
|
||||||
:: win == myid ->
|
|
||||||
leader = myid;
|
|
||||||
nr_leaders++;
|
|
||||||
assert(nr_leaders == 1);
|
|
||||||
:: else ->
|
|
||||||
skip;
|
|
||||||
fi;
|
|
||||||
|
|
||||||
done++;
|
|
||||||
goto restart;
|
|
||||||
}
|
|
||||||
|
|
||||||
init {
|
|
||||||
atomic {
|
|
||||||
run node (nr0,1,zero_one,one_zero,2,zero_two,two_zero);
|
|
||||||
run node (nr1,0,one_zero,zero_one,2,one_two,two_one);
|
|
||||||
run node (nr2,0,two_zero,zero_two,1,two_one,one_two);
|
|
||||||
}
|
|
||||||
do
|
|
||||||
:: true ->
|
|
||||||
done = 0;
|
|
||||||
nr_leaders = 0;
|
|
||||||
leader = udef;
|
|
||||||
nr0!tok; nr1!tok; nr2!tok;
|
|
||||||
done == 3;
|
|
||||||
od;
|
|
||||||
}
|
|
||||||
|
|
@ -1,118 +0,0 @@
|
||||||
/* Echo Election Algorithm with Extinction in an Arbitrary Network. */
|
|
||||||
/* Variation 1: Node 0 wins every time. */
|
|
||||||
|
|
||||||
#define L 10 /* size of buffer */
|
|
||||||
#define udef 3
|
|
||||||
|
|
||||||
#define noLeader (nr_leaders == 0)
|
|
||||||
#define zeroLeads (nr_leaders == 1 && leader == 0)
|
|
||||||
#define oneLeads (nr_leaders == 1 && leader == 1)
|
|
||||||
#define twoLeads (nr_leaders == 1 && leader == 2)
|
|
||||||
#define threeLeads (nr_leaders == 1 && leader == 3)
|
|
||||||
|
|
||||||
mtype = { tok, ldr };
|
|
||||||
chan zero_one = [L] of { mtype, byte};
|
|
||||||
chan zero_two = [L] of { mtype, byte};
|
|
||||||
chan one_zero = [L] of { mtype, byte};
|
|
||||||
chan one_two = [L] of { mtype, byte};
|
|
||||||
chan two_zero = [L] of { mtype, byte};
|
|
||||||
chan two_one = [L] of { mtype, byte};
|
|
||||||
|
|
||||||
chan nr0 = [0] of {mtype, byte};
|
|
||||||
chan nr1 = [0] of {mtype, byte};
|
|
||||||
chan nr2 = [0] of {mtype, byte};
|
|
||||||
|
|
||||||
byte nr_leaders, done, leader;
|
|
||||||
|
|
||||||
inline recvldr ()
|
|
||||||
{
|
|
||||||
if
|
|
||||||
:: lrec == 0 && r != myid ->
|
|
||||||
out1!ldr(r);
|
|
||||||
out2!ldr(r);
|
|
||||||
:: else -> skip;
|
|
||||||
fi;
|
|
||||||
lrec++;
|
|
||||||
win = r;
|
|
||||||
}
|
|
||||||
|
|
||||||
inline recvtok (q,c)
|
|
||||||
{
|
|
||||||
if
|
|
||||||
:: (r+turn)%3 < (caw+turn)%3 ->
|
|
||||||
caw = r;
|
|
||||||
rec = 0;
|
|
||||||
father = q;
|
|
||||||
c!tok(r);
|
|
||||||
:: else -> skip;
|
|
||||||
fi;
|
|
||||||
|
|
||||||
if
|
|
||||||
:: r == caw ->
|
|
||||||
rec++;
|
|
||||||
if
|
|
||||||
:: rec == 2 && caw == myid
|
|
||||||
-> out1!ldr(myid); out2!ldr(myid);
|
|
||||||
:: rec == 2 && caw != myid && father == neigh1
|
|
||||||
-> out1!tok(caw)
|
|
||||||
:: rec == 2 && caw != myid && father == neigh2
|
|
||||||
-> out2!tok(caw)
|
|
||||||
:: else -> skip;
|
|
||||||
fi;
|
|
||||||
:: else -> skip;
|
|
||||||
fi;
|
|
||||||
}
|
|
||||||
|
|
||||||
proctype node (chan nr; byte neigh1; chan out1, in1;
|
|
||||||
byte neigh2; chan out2, in2)
|
|
||||||
{ byte myid = 3 - neigh1 - neigh2;
|
|
||||||
byte caw, rec, father, lrec, win, r, turn;
|
|
||||||
|
|
||||||
xr in1; xr in2;
|
|
||||||
xs out1; xs out2;
|
|
||||||
|
|
||||||
restart:
|
|
||||||
nr?tok(turn);
|
|
||||||
caw = myid; rec = 0; lrec = 0;
|
|
||||||
father = udef; win = udef; r = udef;
|
|
||||||
|
|
||||||
out1!tok(myid);
|
|
||||||
out2!tok(myid);
|
|
||||||
do
|
|
||||||
:: lrec == 2 -> break;
|
|
||||||
:: in1?ldr(r) -> recvldr();
|
|
||||||
:: in2?ldr(r) -> recvldr();
|
|
||||||
:: in1?tok(r) -> recvtok(neigh1,out2);
|
|
||||||
:: in2?tok(r) -> recvtok(neigh2,out1);
|
|
||||||
od;
|
|
||||||
|
|
||||||
if
|
|
||||||
:: win == myid ->
|
|
||||||
leader = myid;
|
|
||||||
nr_leaders++;
|
|
||||||
assert(nr_leaders == 1);
|
|
||||||
:: else ->
|
|
||||||
skip;
|
|
||||||
fi;
|
|
||||||
|
|
||||||
done++;
|
|
||||||
goto restart;
|
|
||||||
}
|
|
||||||
|
|
||||||
init {
|
|
||||||
byte turn = 0;
|
|
||||||
atomic {
|
|
||||||
run node (nr0,1,zero_one,one_zero,2,zero_two,two_zero);
|
|
||||||
run node (nr1,0,one_zero,zero_one,2,one_two,two_one);
|
|
||||||
run node (nr2,0,two_zero,zero_two,1,two_one,one_two);
|
|
||||||
}
|
|
||||||
do
|
|
||||||
:: true ->
|
|
||||||
done = 0;
|
|
||||||
nr_leaders = 0;
|
|
||||||
leader = udef;
|
|
||||||
nr0!tok(turn); nr1!tok(turn); nr2!tok(turn);
|
|
||||||
done == 3;
|
|
||||||
turn = (turn+1)%3;
|
|
||||||
od;
|
|
||||||
}
|
|
||||||
|
|
@ -1,55 +0,0 @@
|
||||||
[](!p0)
|
|
||||||
<>p1 -> (!p0 U p1)
|
|
||||||
[](p2 -> [](!p0))
|
|
||||||
[]((p2 & !p1 & <>p1) -> (!p0 U p1))
|
|
||||||
[](p2 & !p1 -> (!p0 U (p1 | []!p0)))
|
|
||||||
<>(p0)
|
|
||||||
!p1 U ((p0 & !p1) | []!p1)
|
|
||||||
[](!p2) | <>(p2 & <>p0)
|
|
||||||
[](p2 & !p1 -> (!p1 U ((p0 & !p1) | []!p1)))
|
|
||||||
[](p2 & !p1 -> (!p1 U (p0 & !p1)))
|
|
||||||
<>p1 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1)))))))))
|
|
||||||
[]((p2 & <>p1) -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1))))))))))
|
|
||||||
[](p2 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U (p1 | []!p0)) | []p0)))))))))
|
|
||||||
[](p0)
|
|
||||||
<>p1 -> (p0 U p1)
|
|
||||||
[](p2 -> [](p0))
|
|
||||||
[]((p2 & !p1 & <>p1) -> (p0 U p1))
|
|
||||||
[](p2 & !p1 -> (p0 U (p1 | [] p0)))
|
|
||||||
!p0 U (p3 | []!p0)
|
|
||||||
<>p1 -> (!p0 U (p3 | p1))
|
|
||||||
[]!p2 | <>(p2 & (!p0 U (p3 | []!p0)))
|
|
||||||
[]((p2 & !p1 & <>p1) -> (!p0 U (p3 | p1)))
|
|
||||||
[](p2 & !p1 -> (!p0 U ((p3 | p1) | []!p0)))
|
|
||||||
[](p0 -> <>p3)
|
|
||||||
<>p1 -> (p0 -> (!p1 U (p3 & !p1))) U p1
|
|
||||||
[](p2 -> [](p0 -> <>p3))
|
|
||||||
[]((p2 & !p1 & <>p1) -> (p0 -> (!p1 U (p3 & !p1))) U p1)
|
|
||||||
[](p2 & !p1 -> ((p0 -> (!p1 U (p3 & !p1))) U (p1 | [](p0 -> (!p1 U (p3 & !p1))))))
|
|
||||||
<>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))
|
|
||||||
<>p1 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))
|
|
||||||
([]!p2) | (!p2 U (p2 & <>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4)))))
|
|
||||||
[]((p2 & <>p1) -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4)))))
|
|
||||||
[](p2 -> (<>p0 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))))
|
|
||||||
(<>(p3 & X<>p4)) -> ((!p3) U p0)
|
|
||||||
<>p1 -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0))
|
|
||||||
([]!p2) | ((!p2) U (p2 & ((<>(p3 & X<>p4)) -> ((!p3) U p0))))
|
|
||||||
[]((p2 & <>p1) -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0)))
|
|
||||||
[](p2 -> (!(p3 & (!p1) & X(!p1 U (p4 & !p1))) U (p1 | p0) | [](!(p3 & X<>p4))))
|
|
||||||
[] (p3 & X<> p4 -> X(<>(p4 & <> p0)))
|
|
||||||
<>p1 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1
|
|
||||||
[] (p2 -> [] (p3 & X<> p4 -> X(!p4 U (p4 & <> p0))))
|
|
||||||
[] ((p2 & <>p1) -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1)
|
|
||||||
[] (p2 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U (p1 | [] (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0)))))
|
|
||||||
[] (p0 -> <>(p3 & X<>p4))
|
|
||||||
<>p1 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1
|
|
||||||
[] (p2 -> [] (p0 -> (p3 & X<> p4)))
|
|
||||||
[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1)
|
|
||||||
[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U (p1 | [] (p0 -> (p3 & X<> p4))))
|
|
||||||
[] (p0 -> <>(p3 & !p5 & X(!p5 U p4)))
|
|
||||||
<>p1 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1
|
|
||||||
[] (p2 -> [] (p0 -> (p3 & !p5 & X(!p5 U p4))))
|
|
||||||
[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1)
|
|
||||||
[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U (p1 | [] (p0 -> (p3 & !p5 & X(!p5 U p4)))))
|
|
||||||
!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0)
|
|
||||||
<>p2 -> (!p2 U (p2 & (!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0))))
|
|
||||||
|
|
@ -1 +0,0 @@
|
||||||
!(<>[]oneLeader)
|
|
||||||
|
|
@ -1,89 +0,0 @@
|
||||||
/* Dolev, Klawe & Rodeh for leader election in unidirectional ring
|
|
||||||
* `An O(n log n) unidirectional distributed algorithm for extrema
|
|
||||||
* finding in a circle,' J. of Algs, Vol 3. (1982), pp. 245-260
|
|
||||||
*/
|
|
||||||
|
|
||||||
#define elected (nr_leaders > 0)
|
|
||||||
#define noLeader (nr_leaders == 0)
|
|
||||||
#define oneLeader (nr_leaders == 1)
|
|
||||||
|
|
||||||
#define N 5 /* nr of processes (use 5 for demos) */
|
|
||||||
#define I 3 /* node given the smallest number */
|
|
||||||
#define L 10 /* size of buffer (>= 2*N) */
|
|
||||||
|
|
||||||
mtype = { one, two, winner };
|
|
||||||
chan q[N] = [L] of { mtype, byte};
|
|
||||||
|
|
||||||
byte nr_leaders = 0;
|
|
||||||
|
|
||||||
proctype node (chan in, out; byte mynumber)
|
|
||||||
{ bit Active = 1, know_winner = 0;
|
|
||||||
byte nr, maximum = mynumber, neighbourR;
|
|
||||||
|
|
||||||
xr in;
|
|
||||||
xs out;
|
|
||||||
|
|
||||||
printf("MSC: %d\n", mynumber);
|
|
||||||
out!one(mynumber);
|
|
||||||
end: do
|
|
||||||
:: in?one(nr) ->
|
|
||||||
if
|
|
||||||
:: Active ->
|
|
||||||
if
|
|
||||||
:: nr != maximum ->
|
|
||||||
out!two(nr);
|
|
||||||
neighbourR = nr
|
|
||||||
:: else ->
|
|
||||||
/* Raynal p.39: max is greatest number */
|
|
||||||
assert(nr == N);
|
|
||||||
know_winner = 1;
|
|
||||||
out!winner,nr;
|
|
||||||
fi
|
|
||||||
:: else ->
|
|
||||||
out!one(nr)
|
|
||||||
fi
|
|
||||||
|
|
||||||
:: in?two(nr) ->
|
|
||||||
if
|
|
||||||
:: Active ->
|
|
||||||
if
|
|
||||||
:: neighbourR > nr && neighbourR > maximum ->
|
|
||||||
maximum = neighbourR;
|
|
||||||
out!one(neighbourR)
|
|
||||||
:: else ->
|
|
||||||
Active = 0
|
|
||||||
fi
|
|
||||||
:: else ->
|
|
||||||
out!two(nr)
|
|
||||||
fi
|
|
||||||
:: in?winner,nr ->
|
|
||||||
if
|
|
||||||
:: nr != mynumber ->
|
|
||||||
printf("MSC: LOST\n");
|
|
||||||
:: else ->
|
|
||||||
printf("MSC: LEADER\n");
|
|
||||||
nr_leaders++;
|
|
||||||
assert(nr_leaders == 1)
|
|
||||||
fi;
|
|
||||||
if
|
|
||||||
:: know_winner
|
|
||||||
:: else -> out!winner,nr
|
|
||||||
fi;
|
|
||||||
break
|
|
||||||
od
|
|
||||||
}
|
|
||||||
|
|
||||||
init {
|
|
||||||
byte proc;
|
|
||||||
atomic {
|
|
||||||
proc = 1;
|
|
||||||
do
|
|
||||||
:: proc <= N ->
|
|
||||||
run node (q[proc-1], q[proc%N], (N+I-proc)%N+1);
|
|
||||||
proc++
|
|
||||||
:: proc > N ->
|
|
||||||
break
|
|
||||||
od
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
|
|
@ -1,2 +0,0 @@
|
||||||
!((![]<>(r)) -> [](<>p -> <>q))
|
|
||||||
|
|
||||||
|
|
@ -1,155 +0,0 @@
|
||||||
/*
|
|
||||||
* Model of cell-phone handoff strategy in a mobile network.
|
|
||||||
* A translation from the pi-calculus description of this
|
|
||||||
* model presented in:
|
|
||||||
* Fredrik Orava and Joachim Parrow, 'An algebraic verification
|
|
||||||
* of a mobile network,' Formal aspects of computing, 4:497-543 (1992).
|
|
||||||
* For more information on this model, email: joachim@it.kth.se
|
|
||||||
*
|
|
||||||
* See also the simplified version of this model in mobile2
|
|
||||||
*
|
|
||||||
* The ltl property definition for this version is in mobile1.ltl
|
|
||||||
*
|
|
||||||
* to perform the verification with xspin, simply use the ltl property
|
|
||||||
* manager, which will load the above .ltl file by default.
|
|
||||||
* to perform the verificaion from a Unix command line, type:
|
|
||||||
* $ spin -a -N mobile1.ltl mobile1
|
|
||||||
* $ cc -o pan pan.c
|
|
||||||
* $ pan -a
|
|
||||||
*/
|
|
||||||
|
|
||||||
#define p in?[red]
|
|
||||||
#define q out?[red]
|
|
||||||
#define r (BS[a_id]@progress || BS[p_id]@progress)
|
|
||||||
|
|
||||||
mtype = { data, ho_cmd, ho_com, ho_acc, ho_fail, ch_rel, white, red, blue };
|
|
||||||
|
|
||||||
chan in = [1] of { mtype };
|
|
||||||
chan out = [1] of { mtype };
|
|
||||||
|
|
||||||
byte a_id, p_id; /* ids of processes refered to in the property */
|
|
||||||
|
|
||||||
proctype CC(chan fa, fp, l) /* communication controller */
|
|
||||||
{ chan m_old, m_new, x;
|
|
||||||
mtype v;
|
|
||||||
|
|
||||||
do
|
|
||||||
:: in?v ->
|
|
||||||
printf("MSC: DATA\n");
|
|
||||||
fa!data; fa!v
|
|
||||||
:: l?m_new ->
|
|
||||||
fa!ho_cmd; fa!m_new;
|
|
||||||
printf("MSC: HAND-OFF\n");
|
|
||||||
if
|
|
||||||
:: fp?ho_com ->
|
|
||||||
printf("MSC: CH_REL\n");
|
|
||||||
fa!ch_rel; fa?m_old;
|
|
||||||
l!m_old;
|
|
||||||
x = fa; fa = fp; fp = x
|
|
||||||
:: fa?ho_fail ->
|
|
||||||
printf("MSC: FAIL\n");
|
|
||||||
l!m_new
|
|
||||||
fi
|
|
||||||
od
|
|
||||||
}
|
|
||||||
|
|
||||||
proctype HC(chan l, m) /* handover controller */
|
|
||||||
{
|
|
||||||
do
|
|
||||||
:: l!m; l?m
|
|
||||||
od
|
|
||||||
}
|
|
||||||
|
|
||||||
proctype MSC(chan fa, fp, m) /* mobile switching center */
|
|
||||||
{ chan l = [0] of { chan };
|
|
||||||
|
|
||||||
atomic {
|
|
||||||
run HC(l, m);
|
|
||||||
run CC(fa, fp, l)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
proctype BS(chan f, m; bit how) /* base station */
|
|
||||||
{ chan v;
|
|
||||||
|
|
||||||
if
|
|
||||||
:: how -> goto Active
|
|
||||||
:: else -> goto Passive
|
|
||||||
fi;
|
|
||||||
|
|
||||||
Active:
|
|
||||||
printf("MSC: ACTIVE\n");
|
|
||||||
do
|
|
||||||
:: f?data -> f?v; m!data; m!v
|
|
||||||
:: f?ho_cmd -> /* handover command */
|
|
||||||
progress: f?v; m!ho_cmd; m!v;
|
|
||||||
if
|
|
||||||
:: f?ch_rel ->
|
|
||||||
f!m;
|
|
||||||
goto Passive
|
|
||||||
:: m?ho_fail ->
|
|
||||||
printf("MSC: FAILURE\n");
|
|
||||||
f!ho_fail
|
|
||||||
fi
|
|
||||||
od;
|
|
||||||
|
|
||||||
Passive:
|
|
||||||
printf("MSC: PASSIVE\n");
|
|
||||||
m?ho_acc -> f!ho_com;
|
|
||||||
goto Active
|
|
||||||
}
|
|
||||||
|
|
||||||
proctype MS(chan m) /* mobile station */
|
|
||||||
{ chan m_new;
|
|
||||||
mtype v;
|
|
||||||
|
|
||||||
do
|
|
||||||
:: m?data -> m?v; out!v
|
|
||||||
:: m?ho_cmd; m?m_new;
|
|
||||||
if
|
|
||||||
:: m_new!ho_acc; m = m_new
|
|
||||||
:: m!ho_fail
|
|
||||||
fi
|
|
||||||
od
|
|
||||||
}
|
|
||||||
|
|
||||||
proctype P(chan fa, fp)
|
|
||||||
{ chan m = [0] of { mtype };
|
|
||||||
|
|
||||||
atomic {
|
|
||||||
run MSC(fa, fp, m);
|
|
||||||
p_id = run BS(fp, m, 0) /* passive base station */
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
proctype Q(chan fa)
|
|
||||||
{ chan m = [0] of { mtype }; /* mixed use as mtype/chan */
|
|
||||||
|
|
||||||
atomic {
|
|
||||||
a_id = run BS(fa, m, 1); /* active base station */
|
|
||||||
run MS(m)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
active proctype System()
|
|
||||||
{ chan fa = [0] of { mtype }; /* mixed use as mtype/chan */
|
|
||||||
chan fp = [0] of { mtype }; /* mixed use as mtype/chan */
|
|
||||||
|
|
||||||
atomic {
|
|
||||||
run P(fa, fp);
|
|
||||||
run Q(fa)
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
active proctype top()
|
|
||||||
{
|
|
||||||
do
|
|
||||||
:: in!red; in!white; in!blue
|
|
||||||
od
|
|
||||||
}
|
|
||||||
active proctype bot()
|
|
||||||
{
|
|
||||||
do /* deadlock on loss or duplication */
|
|
||||||
:: out?red; out?white; out?blue
|
|
||||||
od
|
|
||||||
}
|
|
||||||
|
|
@ -1 +0,0 @@
|
||||||
!((![]<>(r)) -> [](<>p -> <>q))
|
|
||||||
|
|
@ -1,136 +0,0 @@
|
||||||
/*
|
|
||||||
* Simplified model of cell-phone handoff strategy in a mobile network.
|
|
||||||
* A translation from the pi-calculus description of this
|
|
||||||
* model presented in:
|
|
||||||
* Fredrik Orava and Joachim Parrow, 'An algebraic verification
|
|
||||||
* of a mobile network,' Formal aspects of computing, 4:497-543 (1992).
|
|
||||||
* For more information on this model, email: joachim@it.kth.se
|
|
||||||
*
|
|
||||||
* This version exploits some Promela features to reduce the number
|
|
||||||
* of processes -- which looks better in simulations, and reduces
|
|
||||||
* complexity (by about 60%) in verification.
|
|
||||||
*
|
|
||||||
* See also the more literal version of this model in mobile1.
|
|
||||||
*
|
|
||||||
* The ltl property definition for this version is in mobile2.ltl
|
|
||||||
*
|
|
||||||
* to perform the verification with xspin, simply use the ltl property
|
|
||||||
* manager, which will load the above .ltl file by default.
|
|
||||||
* to perform the verificaion from a Unix command line, type:
|
|
||||||
* $ spin -a -N mobile2.ltl mobile2
|
|
||||||
* $ cc -o pan pan.c
|
|
||||||
* $ pan -a
|
|
||||||
*/
|
|
||||||
|
|
||||||
#define p in?[red]
|
|
||||||
#define q out?[red]
|
|
||||||
#define r (BS[a_id]@progress || BS[p_id]@progress)
|
|
||||||
|
|
||||||
mtype = { data, ho_cmd, ho_com, ho_acc, ho_fail, ch_rel, white, red, blue };
|
|
||||||
|
|
||||||
chan in = [1] of { mtype };
|
|
||||||
chan out = [1] of { mtype };
|
|
||||||
chan fa = [0] of { chan };
|
|
||||||
chan fp = [0] of { chan };
|
|
||||||
chan m1 = [0] of { chan };
|
|
||||||
chan m2 = [0] of { chan };
|
|
||||||
chan l = [0] of { chan };
|
|
||||||
|
|
||||||
byte a_id, p_id; /* ids of processes refered to in the property */
|
|
||||||
|
|
||||||
proctype CC() /* communication controller */
|
|
||||||
{ chan m_old, m_new, x;
|
|
||||||
mtype v;
|
|
||||||
|
|
||||||
do
|
|
||||||
:: in?v ->
|
|
||||||
printf("MSC: DATA\n");
|
|
||||||
fa!data; fa!v
|
|
||||||
:: l?m_new ->
|
|
||||||
fa!ho_cmd; fa!m_new;
|
|
||||||
printf("MSC: HAND-OFF\n");
|
|
||||||
if
|
|
||||||
:: fp?ho_com ->
|
|
||||||
printf("MSC: CH_REL\n");
|
|
||||||
fa!ch_rel; fa?m_old;
|
|
||||||
l!m_old;
|
|
||||||
x = fa; fa = fp; fp = x
|
|
||||||
:: fa?ho_fail ->
|
|
||||||
printf("MSC: FAIL\n");
|
|
||||||
l!m_new
|
|
||||||
fi
|
|
||||||
od
|
|
||||||
}
|
|
||||||
|
|
||||||
proctype HC(chan m) /* handover controller */
|
|
||||||
{
|
|
||||||
do
|
|
||||||
:: l!m; l?m
|
|
||||||
od
|
|
||||||
}
|
|
||||||
|
|
||||||
proctype BS(chan f, m; bit how) /* base station */
|
|
||||||
{ chan v;
|
|
||||||
|
|
||||||
if
|
|
||||||
:: how -> goto Active
|
|
||||||
:: else -> goto Passive
|
|
||||||
fi;
|
|
||||||
|
|
||||||
Active:
|
|
||||||
printf("MSC: ACTIVE\n");
|
|
||||||
do
|
|
||||||
:: f?data -> f?v; m!data; m!v
|
|
||||||
:: f?ho_cmd -> /* handover command */
|
|
||||||
progress: f?v; m!ho_cmd; m!v;
|
|
||||||
if
|
|
||||||
:: f?ch_rel ->
|
|
||||||
f!m;
|
|
||||||
goto Passive
|
|
||||||
:: m?ho_fail ->
|
|
||||||
printf("MSC: FAILURE\n");
|
|
||||||
f!ho_fail
|
|
||||||
fi
|
|
||||||
od;
|
|
||||||
|
|
||||||
Passive:
|
|
||||||
printf("MSC: PASSIVE\n");
|
|
||||||
m?ho_acc -> f!ho_com;
|
|
||||||
goto Active
|
|
||||||
}
|
|
||||||
|
|
||||||
proctype MS(chan m) /* mobile station */
|
|
||||||
{ chan m_new;
|
|
||||||
mtype v;
|
|
||||||
|
|
||||||
do
|
|
||||||
:: m?data -> m?v; out!v
|
|
||||||
:: m?ho_cmd; m?m_new;
|
|
||||||
if
|
|
||||||
:: m_new!ho_acc; m = m_new
|
|
||||||
:: m!ho_fail
|
|
||||||
fi
|
|
||||||
od
|
|
||||||
}
|
|
||||||
|
|
||||||
active proctype System()
|
|
||||||
{
|
|
||||||
atomic {
|
|
||||||
run HC(m1);
|
|
||||||
run CC();
|
|
||||||
p_id = run BS(fp, m1, 0); /* passive base station */
|
|
||||||
a_id = run BS(fa, m2, 1); /* active base station */
|
|
||||||
run MS(m2)
|
|
||||||
}
|
|
||||||
|
|
||||||
end: do
|
|
||||||
:: in!red; in!white; in!blue
|
|
||||||
od
|
|
||||||
}
|
|
||||||
|
|
||||||
active proctype Out()
|
|
||||||
{
|
|
||||||
end: do /* deadlocks if order is disturbed */
|
|
||||||
:: out?red; out?white; out?blue
|
|
||||||
od
|
|
||||||
}
|
|
||||||
|
|
@ -1 +0,0 @@
|
||||||
![] (zune_at_S -> <> zune_at_E)
|
|
||||||
|
|
@ -1,70 +0,0 @@
|
||||||
/*
|
|
||||||
* input: days elapsed since Jan 1, 1980
|
|
||||||
* intended output: year and daynr in current year
|
|
||||||
*
|
|
||||||
* a bug caused all Zune-30 players to freeze on Dec 31, 2008
|
|
||||||
* http://www.zuneboards.com/forums/zune-news/38143-cause-zune-30-leapyear-problem-isolated.html
|
|
||||||
*
|
|
||||||
* Wikepedia:
|
|
||||||
* The bug was in the firmware clock-driver, which was written by Freescale
|
|
||||||
* for their MC13783 PMIC processor. The same bug froze up Toshiba Gigabeat S
|
|
||||||
* media players that share the same hardware and driver.
|
|
||||||
*/
|
|
||||||
|
|
||||||
#define IsLeapYear(y) (((y%4 == 0) && (y%100 != 0)) || (y%400 == 0))
|
|
||||||
|
|
||||||
chan q = [0] of { short };
|
|
||||||
|
|
||||||
active proctype zune()
|
|
||||||
{ short year = 1980;
|
|
||||||
short days;
|
|
||||||
|
|
||||||
end: do
|
|
||||||
:: q?days ->
|
|
||||||
S: do
|
|
||||||
:: days > 365 ->
|
|
||||||
if
|
|
||||||
:: IsLeapYear(year) ->
|
|
||||||
if
|
|
||||||
:: days > 366 ->
|
|
||||||
days = days - 366;
|
|
||||||
year++
|
|
||||||
:: else
|
|
||||||
#ifdef FIX
|
|
||||||
-> break
|
|
||||||
#endif
|
|
||||||
fi
|
|
||||||
:: else ->
|
|
||||||
days = days - 365;
|
|
||||||
year++
|
|
||||||
fi
|
|
||||||
:: else ->
|
|
||||||
break
|
|
||||||
od;
|
|
||||||
E: printf("Year: %d, Day %d\n", year, days)
|
|
||||||
od;
|
|
||||||
/* check that the date is in a valid range */
|
|
||||||
assert(days >= 1 && days <= 366);
|
|
||||||
assert(days < 366 || IsLeapYear(year))
|
|
||||||
}
|
|
||||||
|
|
||||||
init {
|
|
||||||
/* jan 1, 2008 */
|
|
||||||
short days = (2008 - 1980) * 365 + (2008-1980)/4;
|
|
||||||
|
|
||||||
if
|
|
||||||
:: q!days + 365
|
|
||||||
:: q!days + 366
|
|
||||||
:: q!days + 367
|
|
||||||
fi
|
|
||||||
}
|
|
||||||
|
|
||||||
#define zune_at_S zune@S
|
|
||||||
#define zune_at_E zune@E
|
|
||||||
|
|
||||||
/* sample analysis:
|
|
||||||
spin -a zune.pml
|
|
||||||
cc -o pan pan.c
|
|
||||||
./pan -a # find matches of formula
|
|
||||||
spin -t -p -l zune.pml # replay error sequence
|
|
||||||
*/
|
|
||||||
|
|
@ -1,227 +0,0 @@
|
||||||
#!/usr/bin/perl -w
|
|
||||||
#
|
|
||||||
# Copyright (C) 2004 Stefan Schwoon
|
|
||||||
#
|
|
||||||
# This program 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.
|
|
||||||
#
|
|
||||||
# This program 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/>.#
|
|
||||||
#
|
|
||||||
# This script was originally distributed by Schwoon alongside
|
|
||||||
#
|
|
||||||
# @InProceedings{ schwoon.05.tacas,
|
|
||||||
# author = {Stefan Schwoon and Javier Esparza},
|
|
||||||
# title = {A note on on-the-fly verification algorithms.},
|
|
||||||
# booktitle = {Proceedings of the 11th International Conference on Tools
|
|
||||||
# and Algorithms for the Construction and Analysis of Systems
|
|
||||||
# (TACAS'05)},
|
|
||||||
# year = {2005},
|
|
||||||
# series = {Lecture Notes in Computer Science},
|
|
||||||
# publisher = {Springer-Verlag},
|
|
||||||
# month = apr
|
|
||||||
# }
|
|
||||||
#
|
|
||||||
# It has been modified in 2005 by Alexandre Duret-Lutz to
|
|
||||||
# - extract the system's state space instead of the product space
|
|
||||||
# (we want to use the LTL->TGBA translation of Spot, not that of Spin)
|
|
||||||
# - output the state space in Spot's format
|
|
||||||
# - optionally output weak fairness constraints
|
|
||||||
# - allow partial order or not
|
|
||||||
|
|
||||||
use strict;
|
|
||||||
|
|
||||||
my @prop_list;
|
|
||||||
my %props;
|
|
||||||
|
|
||||||
sub usage()
|
|
||||||
{
|
|
||||||
print <<EOF;
|
|
||||||
Usage: pml2tgba.pl [-w] promela-model properties...
|
|
||||||
Extract the state-space of the promela-model, observing properties.
|
|
||||||
|
|
||||||
Options:
|
|
||||||
-w output acceptance conditions to ensure weak fairness
|
|
||||||
-r let Spin reduce the state-space using partial order
|
|
||||||
EOF
|
|
||||||
exit 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
sub create_2n_automaton (@)
|
|
||||||
{
|
|
||||||
my @props = @_;
|
|
||||||
my @res;
|
|
||||||
for my $p (@props)
|
|
||||||
{
|
|
||||||
if (@res)
|
|
||||||
{
|
|
||||||
@res = map { ("$_ && ($p)", "$_ && !($p)") } @res;
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
@res = ("($p)", "!($p)");
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
my $trans = "\n if\n";
|
|
||||||
my $nres = $#res + 1;
|
|
||||||
|
|
||||||
for my $p (@res)
|
|
||||||
{
|
|
||||||
push @prop_list, $p;
|
|
||||||
$trans .= " :: ($p) -> goto T0_init\n";
|
|
||||||
}
|
|
||||||
$trans .= " fi;\n";
|
|
||||||
if ($nres == 0)
|
|
||||||
{
|
|
||||||
push @prop_list, "(1)";
|
|
||||||
}
|
|
||||||
|
|
||||||
return "never {\nT0_init:$trans}\n";
|
|
||||||
}
|
|
||||||
|
|
||||||
usage unless @ARGV;
|
|
||||||
|
|
||||||
my $weak = 0;
|
|
||||||
my $reduce = ' -DNOREDUCE';
|
|
||||||
while (1)
|
|
||||||
{
|
|
||||||
if ($ARGV[0] eq '-w')
|
|
||||||
{
|
|
||||||
$weak = 1;
|
|
||||||
}
|
|
||||||
elsif ($ARGV[0] eq '-r')
|
|
||||||
{
|
|
||||||
$reduce = '';
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
last;
|
|
||||||
}
|
|
||||||
shift;
|
|
||||||
}
|
|
||||||
|
|
||||||
my $model = shift @ARGV;
|
|
||||||
|
|
||||||
# Find out the start of the never claim.
|
|
||||||
# The line numbering changed in Spin 5.2.0.
|
|
||||||
my $model_size = `wc -l <"$model"`;
|
|
||||||
my $neverstartline_spin517 = 3 + $model_size;
|
|
||||||
my $neverstartline_spin520 = 4 + $model_size;
|
|
||||||
my $neverstartline = "($neverstartline_spin517|$neverstartline_spin520)";
|
|
||||||
|
|
||||||
# Create the automaton
|
|
||||||
open NEVER, ">never.$$";
|
|
||||||
print NEVER create_2n_automaton (@ARGV);
|
|
||||||
close NEVER;
|
|
||||||
|
|
||||||
system "spin -a -N never.$$ \"$model\"";
|
|
||||||
unlink "never.$$";
|
|
||||||
system "gcc -DCHECK$reduce -O -o pan pan.c 2>/dev/null";
|
|
||||||
|
|
||||||
# Match Büchi states to propositions
|
|
||||||
my $buechitrans = 'BUG';
|
|
||||||
open PAN, "./pan -d|";
|
|
||||||
while (<PAN>)
|
|
||||||
{
|
|
||||||
last if /^proctype :never/;
|
|
||||||
}
|
|
||||||
while (<PAN>)
|
|
||||||
{
|
|
||||||
next
|
|
||||||
unless (/\s+state\s+\d+\s+-\(tr\s+(\d+)\s*\)->.* line $neverstartline =>/o);
|
|
||||||
# We are assuming that transition are output by -d in the same order
|
|
||||||
# as we specified them in the neverclaim.
|
|
||||||
my $prop = shift @prop_list;
|
|
||||||
$props{$1} = $prop;
|
|
||||||
}
|
|
||||||
close PAN;
|
|
||||||
|
|
||||||
# Build the state graph from pan's DFS output
|
|
||||||
open PAN, "./pan 2>/dev/null |";
|
|
||||||
|
|
||||||
my $dfsstate = 0;
|
|
||||||
my @stack = ();
|
|
||||||
while (<PAN>) {
|
|
||||||
last if (/ New state 0/);
|
|
||||||
}
|
|
||||||
my %acc = ();
|
|
||||||
push @stack, [$dfsstate, $buechitrans, %acc];
|
|
||||||
|
|
||||||
my %allaccs = ();
|
|
||||||
my %trans_list;
|
|
||||||
my $prop = "BUG";
|
|
||||||
while (<PAN>) {
|
|
||||||
if (/^\d*: Down/) {
|
|
||||||
push @stack, [$dfsstate, $buechitrans, %acc];
|
|
||||||
} elsif (/^ New state (\d+)/) {
|
|
||||||
pop @stack;
|
|
||||||
push (@{$trans_list{$dfsstate}}, ["S$dfsstate, S$1, \"$prop\"", %acc]);
|
|
||||||
%acc = ();
|
|
||||||
$dfsstate = $1;
|
|
||||||
push @stack, [$dfsstate, $buechitrans, %acc];
|
|
||||||
} elsif (/^ (Old|Stack) state (\d+)/) {
|
|
||||||
push (@{$trans_list{$dfsstate}}, ["S$dfsstate, S$2, \"$prop\"", %acc]);
|
|
||||||
%acc = ();
|
|
||||||
} elsif (/^ *\d+: proc 0 exec (\d+), \d+ to \d+/) {
|
|
||||||
$buechitrans = $1;
|
|
||||||
$prop = $props{$buechitrans};
|
|
||||||
} elsif (/^ *\d+: proc (\d+) exec \d+, \d+ to \d+/) {
|
|
||||||
$acc{"PR$1"} = 1;
|
|
||||||
$allaccs{"PR$1"} = 1;
|
|
||||||
} elsif (/^\d*: Up/) {
|
|
||||||
pop @stack;
|
|
||||||
($dfsstate, $buechitrans, %acc) = @{$stack[$#stack]};
|
|
||||||
$prop = $props{$buechitrans};
|
|
||||||
}
|
|
||||||
}
|
|
||||||
close PAN;
|
|
||||||
|
|
||||||
unlink "pan", "pan.exe", "pan.c", "pan.h", "pan.b", "pan.t", "pan.m";
|
|
||||||
|
|
||||||
|
|
||||||
print "acc = @{[sort keys %allaccs]};\n" if $weak;
|
|
||||||
for my $state (sort {$a <=> $b} (keys %trans_list))
|
|
||||||
{
|
|
||||||
my %missing = %allaccs;
|
|
||||||
for my $t (@{$trans_list{$state}})
|
|
||||||
{
|
|
||||||
my ($trans, %acc) = @$t;
|
|
||||||
for my $key (keys %acc)
|
|
||||||
{
|
|
||||||
delete $missing{$key};
|
|
||||||
}
|
|
||||||
}
|
|
||||||
for my $t (@{$trans_list{$state}})
|
|
||||||
{
|
|
||||||
my ($trans, %acc) = @$t;
|
|
||||||
print "$trans,";
|
|
||||||
print " @{[sort keys(%acc)]} @{[sort keys(%missing)]}" if $weak;
|
|
||||||
print ";\n";
|
|
||||||
}
|
|
||||||
}
|
|
||||||
exit 0;
|
|
||||||
|
|
||||||
### Setup "GNU" style for perl-mode and cperl-mode.
|
|
||||||
## Local Variables:
|
|
||||||
## perl-indent-level: 2
|
|
||||||
## perl-continued-statement-offset: 2
|
|
||||||
## perl-continued-brace-offset: 0
|
|
||||||
## perl-brace-offset: 0
|
|
||||||
## perl-brace-imaginary-offset: 0
|
|
||||||
## perl-label-offset: -2
|
|
||||||
## cperl-indent-level: 2
|
|
||||||
## cperl-brace-offset: 0
|
|
||||||
## cperl-continued-brace-offset: 0
|
|
||||||
## cperl-label-offset: -2
|
|
||||||
## cperl-extra-newline-before-brace: t
|
|
||||||
## cperl-merge-trailing-else: nil
|
|
||||||
## cperl-continued-statement-offset: 2
|
|
||||||
## End:
|
|
||||||
|
|
@ -162,8 +162,6 @@ AC_CONFIG_FILES([
|
||||||
bench/ltlclasses/Makefile
|
bench/ltlclasses/Makefile
|
||||||
bench/ltl2tgba/Makefile
|
bench/ltl2tgba/Makefile
|
||||||
bench/ltl2tgba/defs
|
bench/ltl2tgba/defs
|
||||||
bench/scc-stats/Makefile
|
|
||||||
bench/split-product/Makefile
|
|
||||||
bench/spin13/Makefile
|
bench/spin13/Makefile
|
||||||
bench/wdba/Makefile
|
bench/wdba/Makefile
|
||||||
doc/Doxyfile
|
doc/Doxyfile
|
||||||
|
|
|
||||||
|
|
@ -31,7 +31,6 @@ tgbaalgos_HEADERS = \
|
||||||
bfssteps.hh \
|
bfssteps.hh \
|
||||||
complete.hh \
|
complete.hh \
|
||||||
compsusp.hh \
|
compsusp.hh \
|
||||||
cutscc.hh \
|
|
||||||
cycles.hh \
|
cycles.hh \
|
||||||
dtgbacomp.hh \
|
dtgbacomp.hh \
|
||||||
degen.hh \
|
degen.hh \
|
||||||
|
|
@ -79,7 +78,6 @@ libtgbaalgos_la_SOURCES = \
|
||||||
bfssteps.cc \
|
bfssteps.cc \
|
||||||
complete.cc \
|
complete.cc \
|
||||||
compsusp.cc \
|
compsusp.cc \
|
||||||
cutscc.cc \
|
|
||||||
cycles.cc \
|
cycles.cc \
|
||||||
dtgbacomp.cc \
|
dtgbacomp.cc \
|
||||||
degen.cc \
|
degen.cc \
|
||||||
|
|
|
||||||
|
|
@ -1,385 +0,0 @@
|
||||||
// -*- coding: utf-8 -*-
|
|
||||||
// Copyright (C) 2009, 2011, 2012, 2013, 2014 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 <iostream>
|
|
||||||
#include <string>
|
|
||||||
#include <queue>
|
|
||||||
#include <algorithm>
|
|
||||||
#include "tgba/tgbaexplicit.hh"
|
|
||||||
#include "cutscc.hh"
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
namespace
|
|
||||||
{
|
|
||||||
static tgba*
|
|
||||||
cut_scc(const tgba* a, const scc_map& m,
|
|
||||||
const std::set<unsigned>& s)
|
|
||||||
{
|
|
||||||
tgba_explicit_string* sub_a = new tgba_explicit_string(a->get_dict());
|
|
||||||
const state* cur = a->get_init_state();
|
|
||||||
std::queue<const state*> tovisit;
|
|
||||||
// Setup
|
|
||||||
state_unicity_table seen;
|
|
||||||
unsigned scc_number;
|
|
||||||
std::string cur_format = a->format_state(cur);
|
|
||||||
std::set<unsigned>::iterator it;
|
|
||||||
// Check if we have at least one accepting SCC.
|
|
||||||
for (it = s.begin(); it != s.end() && !m.accepting(*it); ++it)
|
|
||||||
continue;
|
|
||||||
assert(it != s.end());
|
|
||||||
tovisit.push(seen(cur));
|
|
||||||
sub_a->add_state(cur_format);
|
|
||||||
sub_a->copy_acceptance_conditions_of(a);
|
|
||||||
// If the initial is not part of one of the desired SCC, exit
|
|
||||||
assert(s.find(m.scc_of_state(cur)) != s.end());
|
|
||||||
|
|
||||||
// Perform BFS to visit each state.
|
|
||||||
while (!tovisit.empty())
|
|
||||||
{
|
|
||||||
cur = tovisit.front();
|
|
||||||
tovisit.pop();
|
|
||||||
for (auto sit: a->succ(cur))
|
|
||||||
{
|
|
||||||
cur_format = a->format_state(cur);
|
|
||||||
state* dst = sit->current_state();
|
|
||||||
std::string dst_format = a->format_state(dst);
|
|
||||||
scc_number= m.scc_of_state(dst);
|
|
||||||
// Is the successor included in one of the desired SCC ?
|
|
||||||
if (s.find(scc_number) != s.end())
|
|
||||||
{
|
|
||||||
if (seen.is_new(dst))
|
|
||||||
tovisit.push(dst);
|
|
||||||
state_explicit_string::transition* t =
|
|
||||||
sub_a->create_transition(cur_format, dst_format);
|
|
||||||
sub_a->add_conditions(t, sit->current_condition());
|
|
||||||
bdd acc = sit->current_acceptance_conditions();
|
|
||||||
sub_a->add_acceptance_conditions(t, acc);
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
dst->destroy();
|
|
||||||
}
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return sub_a;
|
|
||||||
}
|
|
||||||
|
|
||||||
static unsigned set_distance(const sccs_set* s1,
|
|
||||||
const sccs_set* s2,
|
|
||||||
const std::vector<unsigned>& scc_sizes)
|
|
||||||
{
|
|
||||||
// Compute the distance between two sets.
|
|
||||||
// Formula is : distance = size(s1) + size(s2) - size(s1 inter s2)
|
|
||||||
std::set<unsigned>::iterator it;
|
|
||||||
std::set<unsigned> result;
|
|
||||||
unsigned inter_sum = 0;
|
|
||||||
std::set_intersection(s1->sccs.begin(), s1->sccs.end(),
|
|
||||||
s2->sccs.begin(), s2->sccs.end(),
|
|
||||||
std::inserter(result, result.begin()));
|
|
||||||
for (it = result.begin(); it != result.end(); ++it)
|
|
||||||
inter_sum += scc_sizes[*it];
|
|
||||||
return s1->size + s2->size - 2*inter_sum;
|
|
||||||
}
|
|
||||||
|
|
||||||
static sccs_set* set_union(sccs_set* s1,
|
|
||||||
sccs_set* s2,
|
|
||||||
const std::vector<unsigned>& scc_sizes)
|
|
||||||
{
|
|
||||||
// Perform the union of two sets.
|
|
||||||
sccs_set* result = new sccs_set;
|
|
||||||
set_union(s1->sccs.begin(), s1->sccs.end(),
|
|
||||||
s2->sccs.begin(), s2->sccs.end(),
|
|
||||||
std::inserter(result->sccs, result->sccs.begin()));
|
|
||||||
result->size = 0;
|
|
||||||
std::set<unsigned>::iterator it;
|
|
||||||
for (it = result->sccs.begin(); it != result->sccs.end(); ++it)
|
|
||||||
result->size += scc_sizes[*it];
|
|
||||||
delete s1;
|
|
||||||
return result;
|
|
||||||
}
|
|
||||||
|
|
||||||
struct recurse_data
|
|
||||||
{
|
|
||||||
std::set<unsigned> seen;
|
|
||||||
std::vector<std::vector<sccs_set* > >* rec_paths;
|
|
||||||
};
|
|
||||||
|
|
||||||
static void find_paths_sub(unsigned init_scc,
|
|
||||||
const scc_map& m,
|
|
||||||
recurse_data& d,
|
|
||||||
const std::vector<unsigned>& scc_sizes)
|
|
||||||
{
|
|
||||||
// Find all the paths from the initial states to an accepting SCC
|
|
||||||
// We need two stacks, one to track the current state, the other to track
|
|
||||||
// the current iterator of this state.
|
|
||||||
std::stack<scc_map::succ_type::const_iterator> it_stack;
|
|
||||||
std::stack<unsigned> scc_stack;
|
|
||||||
std::vector<const scc_map::succ_type*> scc_succ;
|
|
||||||
unsigned scc_count = m.scc_count();
|
|
||||||
scc_succ.reserve(scc_count);
|
|
||||||
d.seen.insert(init_scc);
|
|
||||||
unsigned i;
|
|
||||||
for (i = 0; i < scc_count; ++i)
|
|
||||||
scc_succ.push_back(&(m.succ(i)));
|
|
||||||
// Setup the two stacks with the initial SCC.
|
|
||||||
scc_stack.push(init_scc);
|
|
||||||
it_stack.push(scc_succ[init_scc]->begin());
|
|
||||||
while (!scc_stack.empty())
|
|
||||||
{
|
|
||||||
unsigned cur_scc = scc_stack.top();
|
|
||||||
scc_stack.pop();
|
|
||||||
d.seen.insert(cur_scc);
|
|
||||||
scc_map::succ_type::const_iterator it;
|
|
||||||
// Find the next unvisited successor.
|
|
||||||
for (it = it_stack.top(); it != scc_succ[cur_scc]->end()
|
|
||||||
&& d.seen.find(it->first) != d.seen.end(); ++it)
|
|
||||||
continue;
|
|
||||||
it_stack.pop();
|
|
||||||
// If there are no successors and if the SCC is not accepting, this is
|
|
||||||
// an useless path. Throw it away.
|
|
||||||
if (scc_succ[cur_scc]->begin() == scc_succ[cur_scc]->end()
|
|
||||||
&& !m.accepting(cur_scc))
|
|
||||||
continue;
|
|
||||||
std::vector<std::vector<sccs_set* > >* rec_paths = d.rec_paths;
|
|
||||||
// Is there a successor to process ?
|
|
||||||
if (it != scc_succ[cur_scc]->end())
|
|
||||||
{
|
|
||||||
// Yes, add it to the stack for later processing.
|
|
||||||
unsigned dst = it->first;
|
|
||||||
scc_stack.push(cur_scc);
|
|
||||||
++it;
|
|
||||||
it_stack.push(it);
|
|
||||||
if (d.seen.find(dst) == d.seen.end())
|
|
||||||
{
|
|
||||||
scc_stack.push(dst);
|
|
||||||
it_stack.push(scc_succ[dst]->begin());
|
|
||||||
}
|
|
||||||
}
|
|
||||||
else
|
|
||||||
{
|
|
||||||
// No, all successors have been processed, update the current SCC.
|
|
||||||
for (it = scc_succ[cur_scc]->begin();
|
|
||||||
it != scc_succ[cur_scc]->end(); ++it)
|
|
||||||
{
|
|
||||||
unsigned dst = it->first;
|
|
||||||
std::vector<sccs_set*>::iterator lit;
|
|
||||||
// Extend all the reachable paths by adding the current SCC.
|
|
||||||
for (lit = (*rec_paths)[dst].begin();
|
|
||||||
lit != (*rec_paths)[dst].end(); ++lit)
|
|
||||||
{
|
|
||||||
sccs_set* path = new sccs_set;
|
|
||||||
path->sccs = (*lit)->sccs;
|
|
||||||
path->size = (*lit)->size + scc_sizes[cur_scc];
|
|
||||||
path->sccs.insert(path->sccs.begin(), cur_scc);
|
|
||||||
(*rec_paths)[cur_scc].push_back(path);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
bool has_succ = false;
|
|
||||||
for (it = scc_succ[cur_scc]->begin();
|
|
||||||
it != scc_succ[cur_scc]->end() && !has_succ; ++it)
|
|
||||||
{
|
|
||||||
has_succ = !(*rec_paths)[it->first].empty();
|
|
||||||
}
|
|
||||||
// Create a new path iff the SCC is accepting and not included
|
|
||||||
// in another path.
|
|
||||||
if (m.accepting(cur_scc) && !has_succ)
|
|
||||||
{
|
|
||||||
sccs_set* path = new sccs_set;
|
|
||||||
path->size = scc_sizes[cur_scc];
|
|
||||||
path->sccs.insert(path->sccs.begin(), cur_scc);
|
|
||||||
(*rec_paths)[cur_scc].push_back(path);
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
return;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
std::vector<std::vector<sccs_set* > >* find_paths(tgba* a, const scc_map& m)
|
|
||||||
{
|
|
||||||
unsigned scc_count = m.scc_count();
|
|
||||||
unsigned i;
|
|
||||||
recurse_data d;
|
|
||||||
d.rec_paths = new std::vector<std::vector<sccs_set* > >;
|
|
||||||
for (i = 0; i < scc_count; i++)
|
|
||||||
{
|
|
||||||
std::vector<sccs_set*> list_set;
|
|
||||||
d.rec_paths->push_back(list_set);
|
|
||||||
}
|
|
||||||
// We use a vector to recall the size of all SCCs.
|
|
||||||
std::vector<unsigned> scc_sizes(scc_count, 0);
|
|
||||||
for (i = 0; i < scc_count; ++i)
|
|
||||||
scc_sizes[i] = m.states_of(i).size();
|
|
||||||
state* initial_state = a->get_init_state();
|
|
||||||
unsigned init = m.scc_of_state(initial_state);
|
|
||||||
initial_state->destroy();
|
|
||||||
// Find all interesting pathes in our automaton.
|
|
||||||
find_paths_sub(init, m, d, scc_sizes);
|
|
||||||
|
|
||||||
return d.rec_paths;
|
|
||||||
}
|
|
||||||
|
|
||||||
std::list<tgba*> split_tgba(tgba* a, const scc_map& m,
|
|
||||||
unsigned split_number)
|
|
||||||
{
|
|
||||||
// Main function to split an automaton tgba in split_number sub automata.
|
|
||||||
unsigned i;
|
|
||||||
unsigned scc_count = m.scc_count();
|
|
||||||
unsigned j;
|
|
||||||
std::vector<std::vector<sccs_set* > >* rec_paths = find_paths(a, m);
|
|
||||||
state* initial_state = a->get_init_state();
|
|
||||||
unsigned init = m.scc_of_state(initial_state);
|
|
||||||
initial_state->destroy();
|
|
||||||
std::vector<sccs_set*>* final_sets =&(*rec_paths)[init];
|
|
||||||
if (rec_paths->empty())
|
|
||||||
{
|
|
||||||
std::list<tgba*> empty;
|
|
||||||
return empty;
|
|
||||||
}
|
|
||||||
|
|
||||||
unsigned paths_count = final_sets->size();
|
|
||||||
std::vector< std::vector<unsigned> > dist;
|
|
||||||
for (i = 0; i < paths_count; ++i)
|
|
||||||
{
|
|
||||||
std::vector<unsigned> dist_sub(i, 0);
|
|
||||||
dist.push_back(dist_sub);
|
|
||||||
}
|
|
||||||
|
|
||||||
// We use a vector to recall the size of all SCCs.
|
|
||||||
std::vector<unsigned> scc_sizes(scc_count, 0);
|
|
||||||
for (i = 0; i < scc_count; ++i)
|
|
||||||
scc_sizes[i] = m.states_of(i).size();
|
|
||||||
|
|
||||||
// Compute the distance between all pairs of pathes.
|
|
||||||
for (i = 0; i < paths_count; ++i)
|
|
||||||
for (j = 0; j < i; ++j)
|
|
||||||
{
|
|
||||||
dist[i][j] = set_distance((*final_sets)[i],
|
|
||||||
(*final_sets)[j], scc_sizes);
|
|
||||||
}
|
|
||||||
|
|
||||||
std::vector<bool> is_valid(paths_count, true);
|
|
||||||
unsigned remaining_paths = paths_count;
|
|
||||||
// While the number of subsets is strictly superior to split_number,
|
|
||||||
// merge the two sets with the lowest distance.
|
|
||||||
while (remaining_paths > split_number)
|
|
||||||
{
|
|
||||||
--remaining_paths;
|
|
||||||
unsigned min_i = 1;
|
|
||||||
unsigned min_j = 0;
|
|
||||||
// Initialize with max value.
|
|
||||||
unsigned min = (unsigned)(-1);
|
|
||||||
// Find the two sets with the lowest distance.
|
|
||||||
for (i = 0; i < paths_count; ++i)
|
|
||||||
for (j = 0; j < i; ++j)
|
|
||||||
if (is_valid[i] && is_valid[j])
|
|
||||||
{
|
|
||||||
if (dist[i][j] < min)
|
|
||||||
{
|
|
||||||
min_i = i;
|
|
||||||
min_j = j;
|
|
||||||
min = dist[min_i][min_j];
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
// Merge these sets.
|
|
||||||
(*final_sets)[min_i] = set_union((*final_sets)[min_i],
|
|
||||||
(*final_sets)[min_j],
|
|
||||||
scc_sizes);
|
|
||||||
// The second set is now unused.
|
|
||||||
is_valid[min_j] = false;
|
|
||||||
|
|
||||||
// Update the distances with other sets.
|
|
||||||
for (j = 0; j < min_i; ++j)
|
|
||||||
if (is_valid[min_i] && is_valid[j])
|
|
||||||
dist[min_i][j] = set_distance((*final_sets)[min_i],
|
|
||||||
(*final_sets)[j], scc_sizes);
|
|
||||||
for (i = min_i + 1; i < dist.size(); ++i)
|
|
||||||
if (is_valid[i] && is_valid[min_i])
|
|
||||||
dist[i][min_i] = set_distance((*final_sets)[min_i],
|
|
||||||
(*final_sets)[i], scc_sizes);
|
|
||||||
}
|
|
||||||
std::list<tgba*> result;
|
|
||||||
// Final sets.
|
|
||||||
for (i = 0; i < final_sets->size(); ++i)
|
|
||||||
if (is_valid[i] == true)
|
|
||||||
{
|
|
||||||
//print_set((*final_sets)[i]);
|
|
||||||
result.push_back(cut_scc(a, m, (*final_sets)[i]->sccs));
|
|
||||||
}
|
|
||||||
|
|
||||||
// Free everything.
|
|
||||||
for (i = 0; i < rec_paths->size(); ++i)
|
|
||||||
for (j = 0; j < (*rec_paths)[i].size(); ++j)
|
|
||||||
{
|
|
||||||
delete (*rec_paths)[i][j];
|
|
||||||
}
|
|
||||||
delete rec_paths;
|
|
||||||
return result;
|
|
||||||
}
|
|
||||||
|
|
||||||
unsigned max_spanning_paths(std::vector<sccs_set* >* paths, scc_map& m)
|
|
||||||
{
|
|
||||||
unsigned scc_count = m.scc_count();
|
|
||||||
std::vector<bool> sccs_marked (scc_count, false);
|
|
||||||
std::vector<bool> paths_marked (paths->size(), false);
|
|
||||||
bool done = false;
|
|
||||||
unsigned iter_count = 0;
|
|
||||||
while (!done)
|
|
||||||
{
|
|
||||||
unsigned max = 0;
|
|
||||||
unsigned max_index = 0;
|
|
||||||
unsigned i;
|
|
||||||
for (i = 0; i < paths->size(); ++i)
|
|
||||||
{
|
|
||||||
if (paths_marked[i])
|
|
||||||
continue;
|
|
||||||
unsigned unmarked_sccs = 0;
|
|
||||||
std::set<unsigned>* cur_path = &(*paths)[i]->sccs;
|
|
||||||
std::set<unsigned>::iterator it;
|
|
||||||
for (it = cur_path->begin(); it != cur_path->end(); ++it)
|
|
||||||
{
|
|
||||||
if (!sccs_marked[*it])
|
|
||||||
++unmarked_sccs;
|
|
||||||
}
|
|
||||||
if (unmarked_sccs > max)
|
|
||||||
{
|
|
||||||
max = unmarked_sccs;
|
|
||||||
max_index = i;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
if (max == 0)
|
|
||||||
{
|
|
||||||
done = true;
|
|
||||||
continue;
|
|
||||||
}
|
|
||||||
++iter_count;
|
|
||||||
paths_marked[max_index] = true;
|
|
||||||
std::set<unsigned>* cur_path = &(*paths)[max_index]->sccs;
|
|
||||||
std::set<unsigned>::iterator it;
|
|
||||||
for (it = cur_path->begin(); it != cur_path->end(); ++it)
|
|
||||||
{
|
|
||||||
sccs_marked[*it] = true;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
return iter_count;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
@ -1,48 +0,0 @@
|
||||||
// -*- coding: utf-8 -*-
|
|
||||||
// Copyright (C) 2009, 2013 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/>.
|
|
||||||
|
|
||||||
|
|
||||||
#ifndef SPOT_TGBAALGOS_CUTSCC_HH
|
|
||||||
# define SPOT_TGBAALGOS_CUTSCC_HH
|
|
||||||
|
|
||||||
#include <set>
|
|
||||||
#include <vector>
|
|
||||||
#include "tgba/tgba.hh"
|
|
||||||
#include "tgbaalgos/scc.hh"
|
|
||||||
|
|
||||||
namespace spot
|
|
||||||
{
|
|
||||||
struct sccs_set
|
|
||||||
{
|
|
||||||
std::set<unsigned> sccs;
|
|
||||||
unsigned size;
|
|
||||||
};
|
|
||||||
|
|
||||||
SPOT_API std::vector<std::vector<sccs_set* > >*
|
|
||||||
find_paths(tgba* a, const scc_map& m);
|
|
||||||
|
|
||||||
SPOT_API unsigned
|
|
||||||
max_spanning_paths(std::vector<sccs_set* >* paths, scc_map& m);
|
|
||||||
|
|
||||||
SPOT_API std::list<tgba*>
|
|
||||||
split_tgba(tgba* a, const scc_map& m, unsigned split_number);
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
||||||
#endif // SPOT_TGBAALGOS_CUTSCC_HH
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue