Add 2 benchmarks directories.
Add an algorithm to split an automaton in several automata. * bench/scc-stats: New directory. Contains input files and test program for computing statistics. * bench/split-product: New directory. Contains test program for synchronised product on splitted automata. * bench/split-product/models: New directory. Contains Promela files and LTL formulae that should be verified by the models. * src/tgba/tgbafromfile.cc, src/tgba/tgbafromfile.hh: New files. Small class to avoid long initializations with numerous constants when translating to TGBA many LTL formulae from a given file. * src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh: New file. From a single automaton, create, at most, X sub automata. * src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh: Adjust to compute self-loops count.
This commit is contained in:
Flix Abecassis
parent
a160b3504b
commit
414956c51e
35 changed files with 2989 additions and 5 deletions
23
ChangeLog
23
ChangeLog
|
|
@ -1,9 +1,30 @@
|
|||
2009-07-08 Félix Abecassis <abecassis@lrde.epita.fr>
|
||||
|
||||
Add 2 benchmarks directories.
|
||||
Add an algorithm to split an automaton in several automata.
|
||||
|
||||
* bench/scc-stats: New directory. Contains input files and test
|
||||
program for computing statistics.
|
||||
* bench/split-product: New directory. Contains test program for
|
||||
synchronised product on splitted automata.
|
||||
* bench/split-product/models: New directory. Contains Promela
|
||||
files, and LTL formulae that should be verified by the models.
|
||||
* src/tgba/tgbafromfile.cc, src/tgba/tgbafromfile.hh:
|
||||
New files. Small class to avoid long initializations with numerous
|
||||
constants when translating to TGBA many LTL formulae from a
|
||||
given file.
|
||||
* src/tgbaalgos/cutscc.cc, src/tgbaalgos/cutscc.hh:
|
||||
New file. From a single automaton, create, at most,
|
||||
X sub automata.
|
||||
* src/tgbaalgos/scc.cc, src/tgbaalgos/scc.hh:
|
||||
Adjust to compute self-loops count.
|
||||
|
||||
2009-07-07 Guillaume Sadegh <sadegh@lrde.epita.fr>
|
||||
|
||||
* src/tgba/tgbacomplement.cc: Fix the transformation from
|
||||
Streett to TGBA.
|
||||
* src/tgbatest/complementation.test: Modify tests.
|
||||
|
||||
|
||||
2009-06-17 Alexandre Duret-Lutz <adl@lrde.epita.fr>
|
||||
|
||||
* bench/emptchk/pml2tgba.pl: Adjust to work with Spin 5.2.0.
|
||||
|
|
|
|||
|
|
@ -19,4 +19,4 @@
|
|||
## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||
## 02111-1307, USA.
|
||||
|
||||
SUBDIRS = emptchk gspn-ssp ltl2tgba
|
||||
SUBDIRS = emptchk gspn-ssp ltl2tgba scc-stats split-product
|
||||
|
|
|
|||
32
bench/scc-stats/Makefile.am
Normal file
32
bench/scc-stats/Makefile.am
Normal file
|
|
@ -0,0 +1,32 @@
|
|||
## Copyright (C) 2009 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
## et Marie Curie.
|
||||
##
|
||||
## This file is part of Spot, a model checking library.
|
||||
##
|
||||
## Spot is free software; you can redistribute it and/or modify it
|
||||
## under the terms of the GNU General Public License as published by
|
||||
## the Free Software Foundation; either version 2 of the License, or
|
||||
## (at your option) any later version.
|
||||
##
|
||||
## Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
## License for more details.
|
||||
##
|
||||
## You should have received a copy of the GNU General Public License
|
||||
## along with Spot; see the file COPYING. If not, write to the Free
|
||||
## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||
## 02111-1307, USA.
|
||||
|
||||
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
|
||||
103
bench/scc-stats/README
Normal file
103
bench/scc-stats/README
Normal file
|
|
@ -0,0 +1,103 @@
|
|||
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
|
||||
55
bench/scc-stats/formulae.ltl
Normal file
55
bench/scc-stats/formulae.ltl
Normal file
|
|
@ -0,0 +1,55 @@
|
|||
[](!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))))
|
||||
204
bench/scc-stats/stats.cc
Normal file
204
bench/scc-stats/stats.cc
Normal file
|
|
@ -0,0 +1,204 @@
|
|||
// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire
|
||||
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
|
||||
// Coopératifs (SRC), Université Pierre et Marie Curie.
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
// Spot is free software; you can redistribute it and/or modify it
|
||||
// under the terms of the GNU General Public License as published by
|
||||
// the Free Software Foundation; either version 2 of the License, or
|
||||
// (at your option) any later version.
|
||||
//
|
||||
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
// License for more details.
|
||||
//
|
||||
// You should have received a copy of the GNU General Public License
|
||||
// along with Spot; see the file COPYING. If not, write to the Free
|
||||
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||
// 02111-1307, USA.
|
||||
|
||||
#include <queue>
|
||||
#include <math.h>
|
||||
#include "tgbaalgos/scc.hh"
|
||||
#include "tgbaalgos/cutscc.hh"
|
||||
#include "tgba/tgbafromfile.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
unsigned tgba_size(const tgba* a)
|
||||
{
|
||||
typedef Sgi::hash_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.
|
||||
delete dst;
|
||||
}
|
||||
delete sit;
|
||||
}
|
||||
hash_type::iterator it2;
|
||||
// Free visited states.
|
||||
for (it2 = seen.begin(); it2 != seen.end(); it2++)
|
||||
{
|
||||
delete *it2;
|
||||
}
|
||||
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;
|
||||
bool count_even;
|
||||
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;
|
||||
// Get each LTL formula.
|
||||
spot::ltl_file* formulae = new spot::ltl_file (argv[1], dict);
|
||||
formulae->begin();
|
||||
unsigned k = 0;
|
||||
do
|
||||
{
|
||||
++k;
|
||||
spot::tgba* a = formulae->current_automaton();
|
||||
// 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);
|
||||
delete initial_state;
|
||||
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;
|
||||
formulae->next();
|
||||
} while (!formulae->done());
|
||||
delete formulae;
|
||||
|
||||
// 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());
|
||||
count_even = (count % 2 == 0);
|
||||
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;
|
||||
}
|
||||
155
bench/split-product/Makefile.am
Normal file
155
bench/split-product/Makefile.am
Normal file
|
|
@ -0,0 +1,155 @@
|
|||
## Copyright (C) 2009 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
## département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
## et Marie Curie.
|
||||
##
|
||||
## This file is part of Spot, a model checking library.
|
||||
##
|
||||
## Spot is free software; you can redistribute it and/or modify it
|
||||
## under the terms of the GNU General Public License as published by
|
||||
## the Free Software Foundation; either version 2 of the License, or
|
||||
## (at your option) any later version.
|
||||
##
|
||||
## Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
## License for more details.
|
||||
##
|
||||
## You should have received a copy of the GNU General Public License
|
||||
## along with Spot; see the file COPYING. If not, write to the Free
|
||||
## Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||
## 02111-1307, USA.
|
||||
|
||||
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/cl3serv1fair.tgba \
|
||||
models/cl3serv1Rfair.tgba \
|
||||
models/cl3serv3.tgba \
|
||||
models/cl3serv3R.tgba \
|
||||
models/cl3serv3fair.tgba \
|
||||
models/cl3serv3Rfair.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
|
||||
295
bench/split-product/README
Normal file
295
bench/split-product/README
Normal file
|
|
@ -0,0 +1,295 @@
|
|||
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.
|
||||
|
||||
347
bench/split-product/cutscc.cc
Normal file
347
bench/split-product/cutscc.cc
Normal file
|
|
@ -0,0 +1,347 @@
|
|||
// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire
|
||||
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
|
||||
// Coopératifs (SRC), Université Pierre et Marie Curie.
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
// Spot is free software; you can redistribute it and/or modify it
|
||||
// under the terms of the GNU General Public License as published by
|
||||
// the Free Software Foundation; either version 2 of the License, or
|
||||
// (at your option) any later version.
|
||||
//
|
||||
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
// License for more details.
|
||||
//
|
||||
// You should have received a copy of the GNU General Public License
|
||||
// along with Spot; see the file COPYING. If not, write to the Free
|
||||
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||
// 02111-1307, USA.
|
||||
|
||||
#include <queue>
|
||||
#include <limits>
|
||||
#include <sys/time.h>
|
||||
#include "tgbaalgos/scc.hh"
|
||||
#include "tgba/tgbafromfile.hh"
|
||||
#include "tgbaalgos/dotty.hh"
|
||||
#include "ltlvisit/destroy.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"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
unsigned tgba_size(const tgba* a)
|
||||
{
|
||||
typedef Sgi::hash_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.
|
||||
delete dst;
|
||||
}
|
||||
delete sit;
|
||||
}
|
||||
hash_type::iterator it2;
|
||||
// Free visited states.
|
||||
for (it2 = seen.begin(); it2 != seen.end(); it2++)
|
||||
{
|
||||
delete *it2;
|
||||
}
|
||||
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_file* formulae = new spot::ltl_file (argv[1], dict);
|
||||
formulae->begin();
|
||||
do
|
||||
{
|
||||
++i;
|
||||
spot::tgba* a = formulae->current_automaton();
|
||||
std::cout << "Formula " << i << std::endl;
|
||||
std::cout << formulae->current_formula_string() << std::endl << std::endl;
|
||||
if (argc != 4)
|
||||
{
|
||||
spot::ltl::atomic_prop_set* s;
|
||||
s = spot::ltl::atomic_prop_collect(formulae->current_formula(), 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;
|
||||
std::string next = "----------------------------------------";
|
||||
std::cout << next << next << std::endl;
|
||||
std::cout << std::endl;
|
||||
formulae->next();
|
||||
} while (!formulae->done());
|
||||
delete r;
|
||||
delete dict;
|
||||
delete formulae;
|
||||
std::cout << "Full " << full_sum << "s" << std::endl
|
||||
<< "Cutting " << cut_sum << "s" << std::endl
|
||||
<< "Split " << split_sum << "s" << std::endl;
|
||||
}
|
||||
55
bench/split-product/formulae.ltl
Normal file
55
bench/split-product/formulae.ltl
Normal file
|
|
@ -0,0 +1,55 @@
|
|||
[](!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))))
|
||||
43
bench/split-product/models/cl3serv1.pml
Normal file
43
bench/split-product/models/cl3serv1.pml
Normal file
|
|
@ -0,0 +1,43 @@
|
|||
#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;
|
||||
}
|
||||
43
bench/split-product/models/cl3serv3.pml
Normal file
43
bench/split-product/models/cl3serv3.pml
Normal file
|
|
@ -0,0 +1,43 @@
|
|||
#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
bench/split-product/models/clserv.ltl
Normal file
1
bench/split-product/models/clserv.ltl
Normal file
|
|
@ -0,0 +1 @@
|
|||
!([] (w1 -> <> s1))
|
||||
9
bench/split-product/models/eeaean.ltl
Normal file
9
bench/split-product/models/eeaean.ltl
Normal file
|
|
@ -0,0 +1,9 @@
|
|||
!(<>[](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))))))
|
||||
116
bench/split-product/models/eeaean1.pml
Normal file
116
bench/split-product/models/eeaean1.pml
Normal file
|
|
@ -0,0 +1,116 @@
|
|||
/* 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;
|
||||
}
|
||||
118
bench/split-product/models/eeaean2.pml
Normal file
118
bench/split-product/models/eeaean2.pml
Normal file
|
|
@ -0,0 +1,118 @@
|
|||
/* 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;
|
||||
}
|
||||
55
bench/split-product/models/formulae.ltl
Normal file
55
bench/split-product/models/formulae.ltl
Normal file
|
|
@ -0,0 +1,55 @@
|
|||
[](!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
bench/split-product/models/leader.ltl
Normal file
1
bench/split-product/models/leader.ltl
Normal file
|
|
@ -0,0 +1 @@
|
|||
!(<>[]oneLeader)
|
||||
89
bench/split-product/models/leader.pml
Normal file
89
bench/split-product/models/leader.pml
Normal file
|
|
@ -0,0 +1,89 @@
|
|||
/* 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
|
||||
}
|
||||
}
|
||||
|
||||
2
bench/split-product/models/mobile1.ltl
Normal file
2
bench/split-product/models/mobile1.ltl
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
!((![]<>(r)) -> [](<>p -> <>q))
|
||||
|
||||
155
bench/split-product/models/mobile1.pml
Normal file
155
bench/split-product/models/mobile1.pml
Normal file
|
|
@ -0,0 +1,155 @@
|
|||
/*
|
||||
* 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
bench/split-product/models/mobile2.ltl
Normal file
1
bench/split-product/models/mobile2.ltl
Normal file
|
|
@ -0,0 +1 @@
|
|||
!((![]<>(r)) -> [](<>p -> <>q))
|
||||
136
bench/split-product/models/mobile2.pml
Normal file
136
bench/split-product/models/mobile2.pml
Normal file
|
|
@ -0,0 +1,136 @@
|
|||
/*
|
||||
* 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
bench/split-product/models/zune.ltl
Normal file
1
bench/split-product/models/zune.ltl
Normal file
|
|
@ -0,0 +1 @@
|
|||
![] (zune_at_S -> <> zune_at_E)
|
||||
70
bench/split-product/models/zune.pml
Normal file
70
bench/split-product/models/zune.pml
Normal file
|
|
@ -0,0 +1,70 @@
|
|||
/*
|
||||
* 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
|
||||
*/
|
||||
229
bench/split-product/pml2tgba.pl
Executable file
229
bench/split-product/pml2tgba.pl
Executable file
|
|
@ -0,0 +1,229 @@
|
|||
#!/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 2 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, write to the Free Software
|
||||
# Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA
|
||||
#
|
||||
#
|
||||
# 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:
|
||||
|
|
@ -77,6 +77,8 @@ AC_CONFIG_FILES([
|
|||
bench/gspn-ssp/defs
|
||||
bench/ltl2tgba/Makefile
|
||||
bench/ltl2tgba/defs
|
||||
bench/scc-stats/Makefile
|
||||
bench/split-product/Makefile
|
||||
doc/Doxyfile
|
||||
doc/Makefile
|
||||
iface/gspn/defs
|
||||
|
|
|
|||
|
|
@ -45,7 +45,8 @@ tgba_HEADERS = \
|
|||
tgbaexplicit.hh \
|
||||
tgbaproduct.hh \
|
||||
tgbatba.hh \
|
||||
tgbareduc.hh
|
||||
tgbareduc.hh \
|
||||
tgbafromfile.hh
|
||||
|
||||
noinst_LTLIBRARIES = libtgba.la
|
||||
libtgba_la_SOURCES = \
|
||||
|
|
@ -65,4 +66,5 @@ libtgba_la_SOURCES = \
|
|||
tgbaexplicit.cc \
|
||||
tgbaproduct.cc \
|
||||
tgbatba.cc \
|
||||
tgbareduc.cc
|
||||
tgbareduc.cc \
|
||||
tgbafromfile.cc
|
||||
|
|
|
|||
97
src/tgba/tgbafromfile.cc
Normal file
97
src/tgba/tgbafromfile.cc
Normal file
|
|
@ -0,0 +1,97 @@
|
|||
// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire
|
||||
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
|
||||
// Coopératifs (SRC), Université Pierre et Marie Curie.
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
// Spot is free software; you can redistribute it and/or modify it
|
||||
// under the terms of the GNU General Public License as published by
|
||||
// the Free Software Foundation; either version 2 of the License, or
|
||||
// (at your option) any later version.
|
||||
//
|
||||
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
// License for more details.
|
||||
//
|
||||
// You should have received a copy of the GNU General Public License
|
||||
// along with Spot; see the file COPYING. If not, write to the Free
|
||||
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||
// 02111-1307, USA.
|
||||
|
||||
#include "tgba/public.hh"
|
||||
#include "tgbafromfile.hh"
|
||||
#include "ltlvisit/destroy.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
ltl_file::ltl_file(const char* filename, bdd_dict* dict)
|
||||
{
|
||||
input_file_.open(filename);
|
||||
assert(input_file_.is_open());
|
||||
done_ = false;
|
||||
env_ = &(ltl::default_environment::instance());
|
||||
dict_ = dict;
|
||||
f_ = 0;
|
||||
fm_exprop_opt_ = false;
|
||||
fm_symb_merge_opt_ = true;
|
||||
post_branching_ = false;
|
||||
fair_loop_approx_ = false;
|
||||
containment_ = false;
|
||||
unobservables_ = 0;
|
||||
fm_red_ = ltl::Reduce_None;
|
||||
}
|
||||
|
||||
ltl_file::~ltl_file()
|
||||
{
|
||||
input_file_.close();
|
||||
}
|
||||
|
||||
bool ltl_file::done()
|
||||
{
|
||||
return(input_file_.eof());
|
||||
}
|
||||
|
||||
void ltl_file::next()
|
||||
{
|
||||
if (f_)
|
||||
{
|
||||
ltl::destroy(f_);
|
||||
f_ = 0;
|
||||
}
|
||||
std::string line = "";
|
||||
while (line == "" && !input_file_.eof())
|
||||
getline(input_file_, line);
|
||||
formula_ = line;
|
||||
}
|
||||
|
||||
void ltl_file::begin()
|
||||
{
|
||||
next();
|
||||
}
|
||||
|
||||
tgba* ltl_file::current_automaton()
|
||||
{
|
||||
spot::tgba* a = 0;
|
||||
f_ = spot::ltl::parse(formula_, pel_, *env_, false);
|
||||
if (spot::ltl::format_parse_errors(std::cerr, formula_, pel_))
|
||||
return 0;
|
||||
// Generate the automaton corresponding to the formula
|
||||
a = spot::ltl_to_tgba_fm(f_, dict_, fm_exprop_opt_,
|
||||
fm_symb_merge_opt_, post_branching_,
|
||||
fair_loop_approx_, unobservables_,
|
||||
fm_red_, containment_);
|
||||
return a;
|
||||
}
|
||||
|
||||
ltl::formula* ltl_file::current_formula()
|
||||
{
|
||||
return f_;
|
||||
}
|
||||
|
||||
std::string ltl_file::current_formula_string()
|
||||
{
|
||||
return formula_;
|
||||
}
|
||||
}
|
||||
|
||||
63
src/tgba/tgbafromfile.hh
Normal file
63
src/tgba/tgbafromfile.hh
Normal file
|
|
@ -0,0 +1,63 @@
|
|||
// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire
|
||||
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
|
||||
// Coopératifs (SRC), Université Pierre et Marie Curie.
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
// Spot is free software; you can redistribute it and/or modify it
|
||||
// under the terms of the GNU General Public License as published by
|
||||
// the Free Software Foundation; either version 2 of the License, or
|
||||
// (at your option) any later version.
|
||||
//
|
||||
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
// License for more details.
|
||||
//
|
||||
// You should have received a copy of the GNU General Public License
|
||||
// along with Spot; see the file COPYING. If not, write to the Free
|
||||
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||
// 02111-1307, USA.
|
||||
|
||||
#ifndef SPOT_TGBA_TGBAFROMFILE_HH
|
||||
# define SPOT_TGBA_TGBAFROMFILE_HH
|
||||
#include <iosfwd>
|
||||
#include <fstream>
|
||||
#include "tgba/public.hh"
|
||||
#include "tgbaalgos/ltl2tgba_fm.hh"
|
||||
#include "tgbaalgos/save.hh"
|
||||
#include "ltlparse/public.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
class ltl_file
|
||||
{
|
||||
public:
|
||||
ltl_file(const char* filename, bdd_dict* dict);
|
||||
~ltl_file();
|
||||
bool done();
|
||||
void next();
|
||||
void begin();
|
||||
tgba* current_automaton();
|
||||
std::string current_formula_string();
|
||||
ltl::formula* current_formula();
|
||||
private:
|
||||
bool done_;
|
||||
std::string formula_;
|
||||
ltl::formula* f_;
|
||||
std::ifstream input_file_;
|
||||
ltl::parse_error_list pel_;
|
||||
ltl::environment* env_;
|
||||
bdd_dict* dict_;
|
||||
bool fm_exprop_opt_;
|
||||
bool fm_symb_merge_opt_;
|
||||
bool post_branching_;
|
||||
bool fair_loop_approx_;
|
||||
bool containment_;
|
||||
ltl::atomic_prop_set* unobservables_;
|
||||
int fm_red_;
|
||||
};
|
||||
}
|
||||
|
||||
|
||||
#endif // SPOT_TGBA_TGBAFROMFILE_HH
|
||||
|
|
@ -29,6 +29,7 @@ tgbaalgosdir = $(pkgincludedir)/tgbaalgos
|
|||
|
||||
tgbaalgos_HEADERS = \
|
||||
bfssteps.hh \
|
||||
cutscc.hh \
|
||||
dotty.hh \
|
||||
dottydec.hh \
|
||||
dupexp.hh \
|
||||
|
|
@ -60,6 +61,7 @@ tgbaalgos_HEADERS = \
|
|||
noinst_LTLIBRARIES = libtgbaalgos.la
|
||||
libtgbaalgos_la_SOURCES = \
|
||||
bfssteps.cc \
|
||||
cutscc.cc \
|
||||
dotty.cc \
|
||||
dottydec.cc \
|
||||
dupexp.cc \
|
||||
|
|
|
|||
421
src/tgbaalgos/cutscc.cc
Normal file
421
src/tgbaalgos/cutscc.cc
Normal file
|
|
@ -0,0 +1,421 @@
|
|||
// Copyright (C) 2003, 2004, 2005, 2006, 2007, 2008, 2009 Laboratoire
|
||||
// d'Informatique de Paris 6 (LIP6), département Systèmes Répartis
|
||||
// Coopératifs (SRC), Université Pierre et Marie Curie.
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
// Spot is free software; you can redistribute it and/or modify it
|
||||
// under the terms of the GNU General Public License as published by
|
||||
// the Free Software Foundation; either version 2 of the License, or
|
||||
// (at your option) any later version.
|
||||
//
|
||||
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
// License for more details.
|
||||
//
|
||||
// You should have received a copy of the GNU General Public License
|
||||
// along with Spot; see the file COPYING. If not, write to the Free
|
||||
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||
// 02111-1307, USA.
|
||||
|
||||
#include <iostream>
|
||||
#include <algorithm>
|
||||
#include <set>
|
||||
#include <fstream>
|
||||
#include <sstream>
|
||||
#include <string>
|
||||
#include <queue>
|
||||
#include <limits>
|
||||
#include <math.h>
|
||||
#include <sys/time.h>
|
||||
#include <stdio.h>
|
||||
#include "tgbaalgos/scc.hh"
|
||||
#include "tgba/tgbaexplicit.hh"
|
||||
#include "cutscc.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
tgba* cut_scc(const tgba* a, const scc_map& m,
|
||||
const std::set<unsigned>* s)
|
||||
{
|
||||
tgba_explicit* sub_a = new tgba_explicit(a->get_dict());
|
||||
state* cur = a->get_init_state();
|
||||
std::queue<state*> tovisit;
|
||||
typedef Sgi::hash_set<const state*,
|
||||
state_ptr_hash, state_ptr_equal> hash_type;
|
||||
// Setup
|
||||
hash_type 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(cur);
|
||||
seen.insert(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();
|
||||
tgba_succ_iterator* sit = a->succ_iter(cur);
|
||||
for (sit->first(); !sit->done(); sit->next())
|
||||
{
|
||||
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.find(dst) == seen.end())
|
||||
{
|
||||
tovisit.push(dst);
|
||||
seen.insert(dst); // has_state?
|
||||
}
|
||||
else
|
||||
{
|
||||
delete dst;
|
||||
}
|
||||
tgba_explicit::transition* t =
|
||||
sub_a->create_transition(cur_format, dst_format);
|
||||
sub_a->add_conditions(t, sit->current_condition());
|
||||
sub_a->
|
||||
add_acceptance_conditions(t,
|
||||
sit->current_acceptance_conditions());
|
||||
}
|
||||
else
|
||||
{
|
||||
delete dst;
|
||||
}
|
||||
}
|
||||
delete sit;
|
||||
}
|
||||
|
||||
hash_type::iterator it2;
|
||||
// Free visited states.
|
||||
for (it2 = seen.begin(); it2 != seen.end(); it2++)
|
||||
{
|
||||
delete *it2;
|
||||
}
|
||||
return sub_a;
|
||||
}
|
||||
|
||||
void print_set(const sccs_set* s)
|
||||
{
|
||||
std::cout << "set : ";
|
||||
std::set<unsigned>::iterator vit;
|
||||
for (vit = s->sccs.begin(); vit != s->sccs.end(); ++vit)
|
||||
std::cout << *vit << " ";
|
||||
std::cout << std::endl;
|
||||
}
|
||||
|
||||
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;
|
||||
}
|
||||
|
||||
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;
|
||||
};
|
||||
|
||||
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);
|
||||
delete initial_state;
|
||||
// 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);
|
||||
delete initial_state;
|
||||
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;
|
||||
}
|
||||
}
|
||||
|
||||
47
src/tgbaalgos/cutscc.hh
Normal file
47
src/tgbaalgos/cutscc.hh
Normal file
|
|
@ -0,0 +1,47 @@
|
|||
// Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
|
||||
// département Systèmes Répartis Coopératifs (SRC), Université Pierre
|
||||
// et Marie Curie.
|
||||
//
|
||||
// This file is part of Spot, a model checking library.
|
||||
//
|
||||
// Spot is free software; you can redistribute it and/or modify it
|
||||
// under the terms of the GNU General Public License as published by
|
||||
// the Free Software Foundation; either version 2 of the License, or
|
||||
// (at your option) any later version.
|
||||
//
|
||||
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
||||
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
||||
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
||||
// License for more details.
|
||||
//
|
||||
// You should have received a copy of the GNU General Public License
|
||||
// along with Spot; see the file COPYING. If not, write to the Free
|
||||
// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
|
||||
// 02111-1307, USA.
|
||||
|
||||
|
||||
#ifndef SPOT_TGBAALGOS_CUTSCC_HH
|
||||
# define SPOT_TGBAALGOS_CUTSCC_HH
|
||||
|
||||
#include <iosfwd>
|
||||
#include <set>
|
||||
#include <vector>
|
||||
#include "tgba/public.hh"
|
||||
#include "tgbaalgos/scc.hh"
|
||||
|
||||
namespace spot
|
||||
{
|
||||
struct sccs_set
|
||||
{
|
||||
std::set<unsigned> sccs;
|
||||
unsigned size;
|
||||
};
|
||||
|
||||
std::vector<std::vector<sccs_set* > >* find_paths(tgba* a, const scc_map& m);
|
||||
unsigned max_spanning_paths(std::vector<sccs_set* >* paths, scc_map& m);
|
||||
std::list<tgba*> split_tgba(tgba* a, const scc_map& m,
|
||||
unsigned split_number);
|
||||
|
||||
}
|
||||
|
||||
#endif // SPOT_TGBAALGOS_CUTSCC_HH
|
||||
|
|
@ -109,6 +109,7 @@ namespace spot
|
|||
{
|
||||
// Setup depth-first search from the initial state.
|
||||
{
|
||||
self_loops_ = 0;
|
||||
state* init = aut_->get_init_state();
|
||||
num_ = -1;
|
||||
h_.insert(std::make_pair(init, num_));
|
||||
|
|
@ -172,6 +173,8 @@ namespace spot
|
|||
// We have a successor to look at.
|
||||
// Fetch the values we are interested in...
|
||||
const state* dest = succ->current_state();
|
||||
if (!dest->compare(todo_.top().first))
|
||||
++self_loops_;
|
||||
bdd acc = succ->current_acceptance_conditions();
|
||||
bdd cond = succ->current_condition();
|
||||
// ... and point the iterator to the next successor, for
|
||||
|
|
@ -195,7 +198,7 @@ namespace spot
|
|||
continue;
|
||||
}
|
||||
|
||||
// If we now the state, reuse the previous object.
|
||||
// If we know the state, reuse the previous object.
|
||||
delete dest;
|
||||
dest = spi->first;
|
||||
|
||||
|
|
@ -281,6 +284,11 @@ namespace spot
|
|||
return scc_map_[n].acc;
|
||||
}
|
||||
|
||||
unsigned scc_map::self_loops() const
|
||||
{
|
||||
return self_loops_;
|
||||
}
|
||||
|
||||
const std::list<const state*>& scc_map::states_of(unsigned n) const
|
||||
{
|
||||
assert(scc_map_.size() > n);
|
||||
|
|
@ -354,6 +362,7 @@ namespace spot
|
|||
scc_stats build_scc_stats(const scc_map& m)
|
||||
{
|
||||
scc_stats res;
|
||||
res.self_loops = m.self_loops();
|
||||
res.scc_total = m.scc_count();
|
||||
|
||||
scc_recurse_data d;
|
||||
|
|
|
|||
|
|
@ -54,6 +54,7 @@ namespace spot
|
|||
///
|
||||
/// A terminal dead SCC is a dead SCC without successors.
|
||||
unsigned dead_paths;
|
||||
unsigned self_loops;
|
||||
|
||||
std::ostream& dump(std::ostream& out) const;
|
||||
};
|
||||
|
|
@ -122,6 +123,9 @@ namespace spot
|
|||
/// \pre This should only be called once build_map() has run.
|
||||
unsigned scc_of_state(const state* s) const;
|
||||
|
||||
/// \brief Return the number of self loops in the automaton.
|
||||
unsigned self_loops() const;
|
||||
|
||||
protected:
|
||||
|
||||
int relabel_component();
|
||||
|
|
@ -171,6 +175,7 @@ namespace spot
|
|||
scc_map_type scc_map_; // Map of constructed maximal SCC.
|
||||
// SCC number "n" in H_ corresponds to entry
|
||||
// "n" in SCC_MAP_.
|
||||
unsigned self_loops_; // Self loops count.
|
||||
};
|
||||
|
||||
scc_stats build_scc_stats(const tgba* a);
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue