diff --git a/README b/README index abf4c3466..a14f3f698 100644 --- a/README +++ b/README @@ -181,8 +181,6 @@ bench/ Benchmarks for ... ltl2tgba/ ... LTL-to-Büchi translation algorithms, ltlcounter/ ... translation of a class of LTL formulae, ltlclasses/ ... translation of more classes of LTL formulae, - scc-stats/ ... SCC statistics after translation of LTL formulae, - split-product/ ... parallelizing gain after splitting LTL automata, spin13/ ... compositional suspension and other improvements, wdba/ ... WDBA minimization (for obligation properties). wrap/ Wrappers for other languages. diff --git a/bench/Makefile.am b/bench/Makefile.am index 59beb61b6..073f5f73e 100644 --- a/bench/Makefile.am +++ b/bench/Makefile.am @@ -1,4 +1,4 @@ -## Copyright (C) 2008, 2009, 2010, 2012, 2013 Laboratoire de Recherche +## Copyright (C) 2008, 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche ## et Développement de l'Epita (LRDE). ## Copyright (C) 2005 Laboratoire d'Informatique de Paris 6 (LIP6), ## département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -19,5 +19,4 @@ ## You should have received a copy of the GNU General Public License ## along with this program. If not, see . -SUBDIRS = emptchk ltl2tgba scc-stats split-product ltlcounter \ - ltlclasses wdba spin13 dtgbasat +SUBDIRS = emptchk ltl2tgba ltlcounter ltlclasses wdba spin13 dtgbasat diff --git a/bench/scc-stats/Makefile.am b/bench/scc-stats/Makefile.am deleted file mode 100644 index 0dca53027..000000000 --- a/bench/scc-stats/Makefile.am +++ /dev/null @@ -1,29 +0,0 @@ -## Copyright (C) 2009 Laboratoire de Recherche et Développement -## de l'Epita (LRDE). -## -## This file is part of Spot, a model checking library. -## -## Spot is free software; you can redistribute it and/or modify it -## under the terms of the GNU General Public License as published by -## the Free Software Foundation; either version 3 of the License, or -## (at your option) any later version. -## -## Spot is distributed in the hope that it will be useful, but WITHOUT -## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -## License for more details. -## -## You should have received a copy of the GNU General Public License -## along with this program. If not, see . - -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 diff --git a/bench/scc-stats/README b/bench/scc-stats/README deleted file mode 100644 index 535552536..000000000 --- a/bench/scc-stats/README +++ /dev/null @@ -1,103 +0,0 @@ -This directory contains the input files and test program used to compute basic -statistics on TGBA. - -========== - CONTENTS -========== - -This directory contains: - -* formulae.ltl - - A list of 96 handwritten formulae with their negations. They come - from three sources: - - @InProceedings{ dwyer.98.fmsp, - author = {Matthew B. Dwyer and George S. Avrunin and James C. - Corbett}, - title = {Property Specification Patterns for Finite-state - Verification}, - booktitle = {Proceedings of the 2nd Workshop on Formal Methods in - Software Practice (FMSP'98)}, - publisher = {ACM Press}, - address = {New York}, - editor = {Mark Ardis}, - month = mar, - year = {1998}, - pages = {7--15} - } - - @InProceedings{ etessami.00.concur, - author = {Kousha Etessami and Gerard J. Holzmann}, - title = {Optimizing {B\"u}chi Automata}, - booktitle = {Proceedings of the 11th International Conference on - Concurrency Theory (Concur'00)}, - pages = {153--167}, - year = {2000}, - editor = {C. Palamidessi}, - volume = {1877}, - series = {Lecture Notes in Computer Science}, - address = {Pennsylvania, USA}, - publisher = {Springer-Verlag} - } - - @InProceedings{ somenzi.00.cav, - author = {Fabio Somenzi and Roderick Bloem}, - title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}}, - booktitle = {Proceedings of the 12th International Conference on - Computer Aided Verification (CAV'00)}, - pages = {247--263}, - year = {2000}, - volume = {1855}, - series = {Lecture Notes in Computer Science}, - address = {Chicago, Illinois, USA}, - publisher = {Springer-Verlag} - } - -* full.ltl - - A list of 1000 large randomly generated LTL formulae with ./randtgba. - -======= - USAGE -======= - - Use the stats program. - Usage : ./stats ltl_file - Where ltl_file is a file with a single LTL formula per line. - -========================== - INTERPRETING THE RESULTS -========================== - - Results can be found in file 'results'. - Here is the list of the measured values: - - Accepting Strongly Connected Components. - Total number of accepting SCC. - - Dead Strongly Connected Components. - Total number of dead SCC. - An SCC is dead if no accepting SCC is reachable from it. - - Accepting Paths. - Number of maximal accepting paths. - An path is maximal and accepting if it ends in an accepting - SCC that is only dead (i.e. non accepting) successors, or no - successors at all. - - Dead Paths. - Number of paths to a terminal dead SCC. - A terminal dead SCC is a dead SCC without successors. - - Max Effective Splitting. - A clue to measure the potential effectiveness of splitting the formula. - This is the maximum number of possible sub automata with unique states. - Beyond this threshold, more sub automata can be generated, but all their - states will be included in some of the previous automata. - - Self Loops per State. - Number of self loops. - A self loop is a transition from a state to itself. - - For each of these measured value, we provide the following statistics - computed on all the formulae in ltl_file:\ - - Min - - Max - - Mean - - Median - - Standard Deviation \ No newline at end of file diff --git a/bench/scc-stats/formulae.ltl b/bench/scc-stats/formulae.ltl deleted file mode 100644 index 8cead4155..000000000 --- a/bench/scc-stats/formulae.ltl +++ /dev/null @@ -1,55 +0,0 @@ -[](!p0) -<>p1 -> (!p0 U p1) -[](p2 -> [](!p0)) -[]((p2 & !p1 & <>p1) -> (!p0 U p1)) -[](p2 & !p1 -> (!p0 U (p1 | []!p0))) -<>(p0) -!p1 U ((p0 & !p1) | []!p1) -[](!p2) | <>(p2 & <>p0) -[](p2 & !p1 -> (!p1 U ((p0 & !p1) | []!p1))) -[](p2 & !p1 -> (!p1 U (p0 & !p1))) -<>p1 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1))))))))) -[]((p2 & <>p1) -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1)))))))))) -[](p2 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U (p1 | []!p0)) | []p0))))))))) -[](p0) -<>p1 -> (p0 U p1) -[](p2 -> [](p0)) -[]((p2 & !p1 & <>p1) -> (p0 U p1)) -[](p2 & !p1 -> (p0 U (p1 | [] p0))) -!p0 U (p3 | []!p0) -<>p1 -> (!p0 U (p3 | p1)) -[]!p2 | <>(p2 & (!p0 U (p3 | []!p0))) -[]((p2 & !p1 & <>p1) -> (!p0 U (p3 | p1))) -[](p2 & !p1 -> (!p0 U ((p3 | p1) | []!p0))) -[](p0 -> <>p3) -<>p1 -> (p0 -> (!p1 U (p3 & !p1))) U p1 -[](p2 -> [](p0 -> <>p3)) -[]((p2 & !p1 & <>p1) -> (p0 -> (!p1 U (p3 & !p1))) U p1) -[](p2 & !p1 -> ((p0 -> (!p1 U (p3 & !p1))) U (p1 | [](p0 -> (!p1 U (p3 & !p1)))))) -<>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4))) -<>p1 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4)))) -([]!p2) | (!p2 U (p2 & <>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4))))) -[]((p2 & <>p1) -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))) -[](p2 -> (<>p0 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4)))))) -(<>(p3 & X<>p4)) -> ((!p3) U p0) -<>p1 -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0)) -([]!p2) | ((!p2) U (p2 & ((<>(p3 & X<>p4)) -> ((!p3) U p0)))) -[]((p2 & <>p1) -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0))) -[](p2 -> (!(p3 & (!p1) & X(!p1 U (p4 & !p1))) U (p1 | p0) | [](!(p3 & X<>p4)))) -[] (p3 & X<> p4 -> X(<>(p4 & <> p0))) -<>p1 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1 -[] (p2 -> [] (p3 & X<> p4 -> X(!p4 U (p4 & <> p0)))) -[] ((p2 & <>p1) -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1) -[] (p2 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U (p1 | [] (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))))) -[] (p0 -> <>(p3 & X<>p4)) -<>p1 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1 -[] (p2 -> [] (p0 -> (p3 & X<> p4))) -[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1) -[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U (p1 | [] (p0 -> (p3 & X<> p4)))) -[] (p0 -> <>(p3 & !p5 & X(!p5 U p4))) -<>p1 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1 -[] (p2 -> [] (p0 -> (p3 & !p5 & X(!p5 U p4)))) -[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1) -[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U (p1 | [] (p0 -> (p3 & !p5 & X(!p5 U p4))))) -!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0) -<>p2 -> (!p2 U (p2 & (!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0)))) \ No newline at end of file diff --git a/bench/scc-stats/stats.cc b/bench/scc-stats/stats.cc deleted file mode 100644 index 81e0c75aa..000000000 --- a/bench/scc-stats/stats.cc +++ /dev/null @@ -1,203 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include -#include -#include "tgbaalgos/scc.hh" -#include "tgbaalgos/cutscc.hh" -#include "ltlparse/ltlfile.hh" -#include "tgbaalgos/ltl2tgba_fm.hh" - -namespace spot -{ - unsigned tgba_size(const tgba* a) - { - typedef std::unordered_set hash_type; - hash_type seen; - std::queue tovisit; - // Perform breadth-first search. - state* init = a->get_init_state(); - tovisit.push(init); - seen.insert(init); - unsigned count = 0; - // While there are still states to visit. - while (!tovisit.empty()) - { - ++count; - state* cur = tovisit.front(); - tovisit.pop(); - tgba_succ_iterator* sit = a->succ_iter(cur); - for (sit->first(); !sit->done(); sit->next()) - { - state* dst = sit->current_state(); - // Is it a new state ? - if (seen.find(dst) == seen.end()) - { - // Yes, register the successor for later processing. - tovisit.push(dst); - seen.insert(dst); - } - else - // No, free dst. - dst->destroy(); - } - delete sit; - } - hash_type::iterator it2; - // Free visited states. - for (it2 = seen.begin(); it2 != seen.end(); it2++) - (*it2)->destroy(); - return count; - } -} - -void compute_and_print(std::vector& v, - int count, std::ofstream& output) -{ - int i; - double sum = 0.; - double mean; - double median; - double variance = 0.; - sum = 0; - // Compute mean: sigma(Xi)/n for i=0..n-1. - for (i = 0; i < count; i++) - sum += v[i]; - mean = sum / count; - // Compute variance: sigma((Xi - mean)*(Xi - mean))/n for i=0..n-1. - for (i = 0; i < count; i++) - variance += (v[i] - mean)*(v[i] - mean); - variance = variance / count; - // Compute median: mean of (n-th/2) value and ((n-th/2)+1) value if n even - // else (n-th+1) value if n odd. - if (count % 2 == 0) - median = float(v[count/2] + v[(count/2)+1])/2; - else - median = v[(count+1)/2]; - output << "\tMin = " << v[0] << std::endl; - output << "\tMax = " << v[count-1] << std::endl; - output << "\tMean = " << mean << std::endl; - output << "\tMedian = " << median << std::endl; - output << "\tStandard Deviation = " << sqrt(variance) << std::endl; - output << std::endl; -} - -int main (int argc, char* argv[]) -{ - if (argc != 2) - { - std::cout << "Usage : ./stats file_name" << std::endl; - std::cout << "There must be one LTL formula per line." << std::endl; - return 1; - } - std::ofstream output; - output.open("results"); - spot::bdd_dict* dict = new spot::bdd_dict(); - unsigned count = 0; - std::vector acc_scc; - std::vector dead_scc; - std::vector acc_paths; - std::vector dead_paths; - std::vector spanning_paths; - std::vector self_loops; - unsigned k = 0; - // Get each LTL formula. - spot::ltl::ltl_file formulae(argv[1]); - while (const spot::ltl::formula* f = formulae.next()) - { - ++k; - spot::tgba* a = ltl_to_tgba_fm(f, dict, /* exprop */ true); - f->destroy(); - // Get number of spanning paths. - spot::scc_map m (a); - m.build_map(); - spot::state* initial_state = a->get_init_state(); - unsigned init = m.scc_of_state(initial_state); - initial_state->destroy(); - std::vector >* paths = find_paths(a, m); - unsigned spanning_count =spot::max_spanning_paths(&(*paths)[init], m); - spanning_paths.push_back(double(spanning_count)); - // Get characteristics from automaton. - spot::scc_stats stat; - stat = build_scc_stats(a); - - // Add those characteristics to our arrays. - acc_scc.push_back(double(stat.acc_scc)); - dead_scc.push_back(double(stat.dead_scc)); - acc_paths.push_back(double(stat.acc_paths)); - dead_paths.push_back(double(stat.dead_paths)); - self_loops.push_back(double(stat.self_loops)/tgba_size(a)); - ++count; - delete a; - unsigned i; - unsigned j; - for (i = 0; i < paths->size(); ++i) - for (j = 0; j < (*paths)[i].size(); ++j) - delete (*paths)[i][j]; - delete paths; - } - - if (count == 0) - { - std::cerr << "Nothing read." << std::endl; - exit(1); - } - - // We could have inserted at the right place instead of - // sorting at the end. - // Sorting allows us to find the extrema and - // the median of the distribution. - sort(acc_scc.begin(), acc_scc.end()); - sort(dead_scc.begin(), dead_scc.end()); - sort(acc_paths.begin(), acc_paths.end()); - sort(spanning_paths.begin(), spanning_paths.end()); - sort(dead_paths.begin(), dead_paths.end()); - sort(self_loops.begin(), self_loops.end()); - output << "Parsed Formulae : " << count << std::endl << std::endl; - - // Accepting SCCs - output << "Accepting SCCs:" << std::endl; - compute_and_print(acc_scc, count, output); - - // Dead SCCs - output << "Dead SCCs:" << std::endl; - compute_and_print(dead_scc, count, output); - - // Accepting Paths - output << "Accepting Paths:" << std::endl; - compute_and_print(acc_paths, count, output); - - // Dead Paths - output << "Dead Paths:" << std::endl; - compute_and_print(dead_paths, count, output); - - // Max Effective Splitting - output << "Max effective splitting:" << std::endl; - compute_and_print(spanning_paths, count, output); - - // Self loops - output << "Self loops per State:" << std::endl; - compute_and_print(self_loops, count, output); - - std::cout << "Statistics generated in file results." << std::endl; - output.close(); - delete dict; - return 0; -} diff --git a/bench/split-product/Makefile.am b/bench/split-product/Makefile.am deleted file mode 100644 index 92764910d..000000000 --- a/bench/split-product/Makefile.am +++ /dev/null @@ -1,148 +0,0 @@ -## Copyright (C) 2009, 2010 Laboratoire de Recherche et Développement -## de l'Epita (LRDE). -## -## This file is part of Spot, a model checking library. -## -## Spot is free software; you can redistribute it and/or modify it -## under the terms of the GNU General Public License as published by -## the Free Software Foundation; either version 3 of the License, or -## (at your option) any later version. -## -## Spot is distributed in the hope that it will be useful, but WITHOUT -## ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -## or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -## License for more details. -## -## You should have received a copy of the GNU General Public License -## along with this program. If not, see . - -PML2TGBA = $(PERL) $(srcdir)/pml2tgba.pl - -RES = cut-results - -AM_CPPFLAGS = -I$(srcdir)/../../src $(BUDDY_CPPFLAGS) -AM_CXXFLAGS = $(WARNING_CXXFLAGS) -LDADD = ../../src/libspot.la - -dist_noinst_SCRIPTS = \ - pml2tgba.pl - -noinst_PROGRAMS = \ - cutscc - -cutscc_SOURCES = cutscc.cc - -nodist_noinst_DATA = \ - models/cl3serv1.tgba \ - models/cl3serv1R.tgba \ - models/cl3serv3.tgba \ - models/cl3serv3R.tgba \ - models/eeaean1.tgba \ - models/eeaean1R.tgba \ - models/eeaean2.tgba \ - models/eeaean2R.tgba \ - models/leader.tgba \ - models/leaderR.tgba \ - models/mobile1.tgba \ - models/mobile1R.tgba \ - models/mobile2.tgba \ - models/mobile2R.tgba \ - models/zune.tgba \ - models/zuneR.tgba - -models/cl3serv1.tgba: $(srcdir)/models/cl3serv1.pml - $(mkdir_p) models - $(PML2TGBA) $(srcdir)/models/cl3serv1.pml w1 s1 >$@ - -models/cl3serv1R.tgba: $(srcdir)/models/cl3serv1.pml - $(mkdir_p) models - $(PML2TGBA) -r $(srcdir)/models/cl3serv1.pml w1 s1 >$@ - -models/cl3serv3.tgba: $(srcdir)/models/cl3serv3.pml - $(mkdir_p) models - $(PML2TGBA) $(srcdir)/models/cl3serv3.pml w1 s1 >$@ - -models/cl3serv3R.tgba: $(srcdir)/models/cl3serv3.pml - $(mkdir_p) models - $(PML2TGBA) -r $(srcdir)/models/cl3serv3.pml w1 s1 >$@ - -models/eeaean1.tgba: $(srcdir)/models/eeaean1.pml - $(mkdir_p) models - $(PML2TGBA) $(srcdir)/models/eeaean1.pml \ - noLeader zeroLeads oneLeads twoLeads threeLeads >$@ - -models/eeaean1R.tgba: $(srcdir)/models/eeaean1.pml - $(mkdir_p) models - $(PML2TGBA) -r $(srcdir)/models/eeaean1.pml \ - noLeader zeroLeads oneLeads twoLeads threeLeads >$@ - -models/eeaean2.tgba: $(srcdir)/models/eeaean2.pml - $(mkdir_p) models - $(PML2TGBA) $(srcdir)/models/eeaean2.pml \ - noLeader zeroLeads oneLeads twoLeads threeLeads >$@ - -models/eeaean2R.tgba: $(srcdir)/models/eeaean2.pml - $(mkdir_p) models - $(PML2TGBA) -r $(srcdir)/models/eeaean2.pml \ - noLeader zeroLeads oneLeads twoLeads threeLeads >$@ - -models/leader.tgba: $(srcdir)/models/leader.pml - $(mkdir_p) models - $(PML2TGBA) $(srcdir)/models/leader.pml \ - elected noLeader oneLeader >$@ - -models/leaderR.tgba: $(srcdir)/models/leader.pml - $(mkdir_p) models - $(PML2TGBA) -r $(srcdir)/models/leader.pml \ - elected noLeader oneLeader >$@ - -models/mobile1.tgba: $(srcdir)/models/mobile1.pml - $(mkdir_p) models - $(PML2TGBA) $(srcdir)/models/mobile1.pml \ - p q r >$@ - -models/mobile1R.tgba: $(srcdir)/models/mobile1.pml - $(mkdir_p) models - $(PML2TGBA) -r $(srcdir)/models/mobile1.pml \ - p q r >$@ - -models/mobile2.tgba: $(srcdir)/models/mobile2.pml - $(mkdir_p) models - $(PML2TGBA) $(srcdir)/models/mobile2.pml \ - p q r >$@ - -models/mobile2R.tgba: $(srcdir)/models/mobile2.pml - $(mkdir_p) models - $(PML2TGBA) -r $(srcdir)/models/mobile2.pml \ - p q r >$@ - -models/zune.tgba: $(srcdir)/models/zune.pml - $(mkdir_p) models - $(PML2TGBA) $(srcdir)/models/zune.pml \ - zune_at_S zune_at_E >$@ - -models/zuneR.tgba: $(srcdir)/models/zune.pml - $(mkdir_p) models - $(PML2TGBA) -r $(srcdir)/models/zune.pml \ - zune_at_S zune_at_E >$@ - -CLEANFILES = $(nodist_noinst_DATA) - -bench: $(noinst_PROGRAMS) - mkdir cut-results 2> /dev/null || true - ./cutscc models/clserv.ltl 4 models/cl3serv1.tgba > $(RES)/cl3serv1 - ./cutscc models/clserv.ltl 4 models/cl3serv1R.tgba > $(RES)/cl3serv1R - ./cutscc models/clserv.ltl 4 models/cl3serv3.tgba > $(RES)/cl3serv3 - ./cutscc models/clserv.ltl 4 models/cl3serv3R.tgba > $(RES)/cl3serv3R - ./cutscc models/eeaean.ltl 4 models/eeaean1.tgba > $(RES)/eeaean1 - ./cutscc models/eeaean.ltl 4 models/eeaean1R.tgba > $(RES)/eeaean1R - ./cutscc models/eeaean.ltl 4 models/eeaean2.tgba > $(RES)/eeaean2 - ./cutscc models/eeaean.ltl 4 models/eeaean2R.tgba > $(RES)/eeaean2R - ./cutscc models/leader.ltl 4 models/leader.tgba > $(RES)/leader - ./cutscc models/leader.ltl 4 models/leaderR.tgba > $(RES)/leaderR - ./cutscc models/mobile1.ltl 4 models/mobile1.tgba > $(RES)/mobile1 - ./cutscc models/mobile1.ltl 4 models/mobile1R.tgba > $(RES)/mobile1R - ./cutscc models/mobile2.ltl 4 models/mobile2.tgba > $(RES)/mobile2 - ./cutscc models/mobile2.ltl 4 models/mobile2R.tgba > $(RES)/mobile2R - ./cutscc models/zune.ltl 4 models/zune.tgba > $(RES)/zune - ./cutscc models/zune.ltl 4 models/zuneR.tgba > $(RES)/zuneR diff --git a/bench/split-product/README b/bench/split-product/README deleted file mode 100644 index 0718617f6..000000000 --- a/bench/split-product/README +++ /dev/null @@ -1,295 +0,0 @@ -This directory contains the input files and test program used to produce -the measures for our new method consisting in splitting the automaton -corresponding to the formula in order to obtain smaller synchronised product. -This new method could lead to parallel computation of emptiness checks for -possibly faster results. - -========== - CONTENTS -========== - -This directory contains: - -* models/cl3serv1.pml -* models/cl3serv3.pml - - Two simple client/server promela examples. - -* models/clserv.ltl - - An LTL formula to verify on these examples. - -* models/eeaean1.pml -* models/eeaean2.pml - - Variations of the leader election protocol with extinction from - Tel, Introduction to Distributed Algorithms, 1994, Chapter 7. The - network in the model consists of three nodes. In Variant 1, the - same node wins every time, in Variant 2, each node gets a turn at - winning the election. These specifications were originally - distributed alongside - - @InProceedings{ schwoon.05.tacas, - author = {Stefan Schwoon and Javier Esparza}, - title = {A note on on-the-fly verification algorithms.}, - booktitle = {Proceedings of the 11th International Conference - on Tools and Algorithms for the Construction and - Analysis of Systems - (TACAS'05)}, - year = {2005}, - series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag}, - month = apr - } - -* models/eeaean.ltl - - Sample properties for the leader election protocols. These come from - - @InProceedings{ geldenhuys.04.tacas, - author = {Jaco Geldenhuys and Antti Valmari}, - title = {Tarjan's Algorithm Makes On-the-Fly {LTL} Verification - More Efficient}, - booktitle = {Proceedings of the 10th International Conference on - Tools and Algorithms for the Construction and Analysis - of Systems - (TACAS'04)}, - editor = {Kurt Jensen and Andreas Podelski}, - pages = {205--219}, - year = {2004}, - publisher = {Springer-Verlag}, - series = {Lecture Notes in Computer Science}, - volume = {2988}, - isbn = {3-540-21299-X} - } - -* formulae.ltl - - A list of 96 handwritten formulae with their negations. They come - from three sources: - - @InProceedings{ dwyer.98.fmsp, - author = {Matthew B. Dwyer and George S. Avrunin and James C. - Corbett}, - title = {Property Specification Patterns for Finite-state - Verification}, - booktitle = {Proceedings of the 2nd Workshop on Formal Methods in - Software Practice (FMSP'98)}, - publisher = {ACM Press}, - address = {New York}, - editor = {Mark Ardis}, - month = mar, - year = {1998}, - pages = {7--15} - } - - @InProceedings{ etessami.00.concur, - author = {Kousha Etessami and Gerard J. Holzmann}, - title = {Optimizing {B\"u}chi Automata}, - booktitle = {Proceedings of the 11th International Conference on - Concurrency Theory (Concur'00)}, - pages = {153--167}, - year = {2000}, - editor = {C. Palamidessi}, - volume = {1877}, - series = {Lecture Notes in Computer Science}, - address = {Pennsylvania, USA}, - publisher = {Springer-Verlag} - } - - @InProceedings{ somenzi.00.cav, - author = {Fabio Somenzi and Roderick Bloem}, - title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}}, - booktitle = {Proceedings of the 12th International Conference on - Computer Aided Verification (CAV'00)}, - pages = {247--263}, - year = {2000}, - volume = {1855}, - series = {Lecture Notes in Computer Science}, - address = {Chicago, Illinois, USA}, - publisher = {Springer-Verlag} - } - -* models/mobile1.pml - - File found in /Spin/Test/ - Model of cell-phone handoff strategy in a mobile network. - A translation from the pi-calculus description of this model presented in: - - @ARTICLE{ Orava91analgebraic, - author = {Fredrik Orava and Joachim Parrow}, - title = {An Algebraic Verification of a Mobile Network}, - journal = {Formal Aspects of Computing}, - year = {1991}, - volume = {4}, - pages = {497--543} - } - -* models/mobile2.pml - - File found in /Spin/Test/ - Simplified model of cell-phone handoff strategy in a mobile network. - A translation from the pi-calculus description of this model presented in - the same article as above. - -* models/leader.pml - - File found in /Spin/Test/ - O(n log n) algorithm for leader election in unidirectional ring. - Presented in: - - @InProceedings{Afek97self-stabilizingunidirectional, - author = {Yehuda Afek and Anat Bremler}, - title = {Self-Stabilizing Unidirectional Network Algorithms - by Power-Supply}, - booktitle = {Chicago Journal of Theoretical Computer Science}, - year = {1997}, - pages = {111--120}, - publisher = {The MIT Press} - } - -* models/zune.pml - - File found in Spin/Test/ - A bug caused all Zune-30 players to freeze on Dec 31, 2008 - http://www.zuneboards.com/forums/zune-news/38143-cause-zune-30-leapyear-problem-isolated.html - The bug was in the firmware clock-driver, which was written by Freescale - for their MC13783 PMIC processor. - input: days elapsed since Jan 1, 1980 - intended output: year and daynr in current year - -* models/cl3serv1.tgba -* models/cl3serv3.tgba -* models/cl3serv1R.tgba -* models/cl3serv3R.tgba -* models/eeaean1.tgba (12MB) -* models/eeaean2.tgba (38MB) -* models/eeaean1R.tgba -* models/eeaean2R.tgba -* models/leader.tgba -* models/leaderR.tgba -* models/mobile1.tgba -* models/mobile1R.tgba -* models/mobile2.tgba -* models/mobile2R.tgba -* models/zune.tgba -* models/zumeR.tgba - - The corresponding TGBA for the Promela models introduced above. - They were translated by pml2tgba.pl (located in bench/emptchk/) - into an input format readable by SPOT. - Promela inputs can be translated in 4 different graphs. - For instance eeaean1.pml is translated as - - eeaean1.tgba full translation - - eeaean1R.tgba reduced translation - The "reduced" translation uses Spin's partial order reductions. - -* results/ - - For each .tgba model in models you can find a simple text file - named . - 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. - diff --git a/bench/split-product/cutscc.cc b/bench/split-product/cutscc.cc deleted file mode 100644 index b8f1888ab..000000000 --- a/bench/split-product/cutscc.cc +++ /dev/null @@ -1,343 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include -#include -#include -#include "tgbaalgos/scc.hh" -#include "ltlparse/ltlfile.hh" -#include "ltlvisit/tostring.hh" -#include "tgbaalgos/dotty.hh" -#include "tgbaalgos/randomgraph.hh" -#include "tgbaalgos/emptiness.hh" -#include "tgba/tgbaproduct.hh" -#include "tgbaalgos/replayrun.hh" -#include "tgbaalgos/emptiness_stats.hh" -#include "ltlvisit/apcollect.hh" -#include "tgbaparse/public.hh" -#include "tgbaalgos/cutscc.hh" -#include "tgbaalgos/ltl2tgba_fm.hh" - -namespace spot -{ - unsigned tgba_size(const tgba* a) - { - typedef std::unordered_set hash_type; - hash_type seen; - std::queue tovisit; - // Perform breadth-first search. - state* init = a->get_init_state(); - tovisit.push(init); - seen.insert(init); - unsigned count = 0; - // While there are still states to visit. - while (!tovisit.empty()) - { - ++count; - state* cur = tovisit.front(); - tovisit.pop(); - tgba_succ_iterator* sit = a->succ_iter(cur); - for (sit->first(); !sit->done(); sit->next()) - { - state* dst = sit->current_state(); - // Is it a new state ? - if (seen.find(dst) == seen.end()) - { - // Yes, register the successor for later processing. - tovisit.push(dst); - seen.insert(dst); - } - else - // No, free dst. - dst->destroy(); - } - delete sit; - } - hash_type::iterator it2; - // Free visited states. - for (it2 = seen.begin(); it2 != seen.end(); it2++) - (*it2)->destroy(); - return count; - } -} - -void TimerReset(struct timeval& start) -{ - // Initialize timer with the current time. - gettimeofday(&start, 0); -} - -double TimerGetElapsedTime(struct timeval& start) -{ - // Compute the diferrence between now and the time when start was initialized. - double t1, t2; - struct timeval end; - TimerReset(end); - t1 = (double)start.tv_sec + (double)start.tv_usec*0.000001; - t2 = (double)end.tv_sec + (double)end.tv_usec*0.000001; - - return t2 - t1; -} - -bool accepting_path(spot::tgba* a, std::ostream& output, bool do_print) -{ - const char* err; - spot::emptiness_check_instantiator* inst; - inst = spot::emptiness_check_instantiator::construct("Cou99", &err); - spot::emptiness_check* ec = inst->instantiate(a); - spot::emptiness_check_result* acc; - acc = ec->check(); - spot::tgba_run* run; - - if (acc) - { - run = acc->accepting_run(); - //const spot::unsigned_statistics* stats = acc->statistics(); - //spot::Replay_tgba_run(output, acc->automaton(), run); - if (do_print) - ec->print_stats(output); - delete run; - delete acc; - } - else if (do_print) - std::cout << "No accepting path." << std::endl; - delete inst; - delete ec; - return acc != 0; -} - -int main(int argc, char* argv[]) -{ - if (argc > 4) - { - std::cout << "Usage ./cutscc file_name split_count [model_file]" - << std::endl; - return 1; - } - std::ofstream out_dot ("auto.dot"); - std::cout.setf (std::ios::fixed); - bool print_size = true; - bool print_time = true; - bool print_ec = true; - int i = 0; - int split_count = atoi(argv[2]); - std::vector accepting_vector; - accepting_vector.reserve(10000); - double split_sum = 0.; - double full_sum = 0.; - double cut_sum = 0.; - spot::tgba* r = 0; - spot::ltl::environment& env(spot::ltl::default_environment::instance()); - spot::bdd_dict* dict = new spot::bdd_dict(); - if (argc == 4) - { - spot::tgba_parse_error_list error_list; - r = spot::tgba_parse(argv[3], error_list, dict, env, env, false); - if (print_size) - std::cout << "Reference automaton has " << tgba_size(r) - << " states." << std::endl - <<"Trying to split each automaton in " << split_count - << " sub automata." << std::endl; - } - // iter_count is the number of iterations done to increase precision. - unsigned iter_count = 1; - std::cout << "Each operation is repeated " << iter_count - << " times to improve precision." << std::endl << std::endl; - - spot::ltl::ltl_file formulae(argv[1]); - while (const spot::ltl::formula* f = formulae.next()) - { - spot::tgba* a = ltl_to_tgba_fm(f, dict, /* exprop */ true); - ++i; - std::cout << "Formula " << i << std::endl; - std::cout << spot::ltl::to_string(f) << std::endl << std::endl; - if (argc != 4) - { - spot::ltl::atomic_prop_set* s; - s = spot::ltl::atomic_prop_collect(f, 0); - spot::ltl::atomic_prop_set::iterator sit; - delete r; - r = spot::random_graph(10000, 0.0001, s, dict, 0, 0.15, 0.5); - delete s; - } - spot::scc_map m (a); - m.build_map(); - - spot::tgba* res = 0; - - // Simplify the tgba to delete useless pathes - if (argc != 4) - { - spot::tgba* tmp = a; - a = spot::split_tgba(a, m, 1).front(); - delete tmp; - } - - struct timeval start; - double elapsed = 0.; - bool full_result; - unsigned j; - for (j = 0; j < iter_count; j++) - { - // Measure the mean computing time for the product with our full - // automaton. - TimerReset(start); - res = new spot::tgba_product(r, a); - full_result = accepting_path(res, std::cout, false); - elapsed += TimerGetElapsedTime(start); - delete res; - } - double full_time = elapsed / iter_count; - full_sum += full_time; - // Compute again for printing purposes only. - res = new spot::tgba_product(r, a); - - unsigned full_size; - if (print_size) - { - full_size = tgba_size(res); - std::cout << "Full Product : " << full_size << " states"; - } - if (print_time) - { - std::cout << " in " << elapsed / iter_count << "s"; - } - std::cout << std::endl; - if (print_ec) - { - accepting_path(res, std::cout, true); - std::cout << std::endl; - } - delete res; - - double cut_time = 0.; - std::list 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::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::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::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 = (elapsedmax) ? 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::iterator lit; - for (lit = splitted.begin(); lit != splitted.end(); lit++) - delete *lit; - if (accepting_vector[i] != full_result) - std::cout << "Disagree !" << std::endl; - split_sum += (accepting_vector[i]) ? min:max; - - delete a; - f->destroy(); - std::string next = "----------------------------------------"; - std::cout << next << next << std::endl; - std::cout << std::endl; - } - delete r; - delete dict; - std::cout << "Full " << full_sum << "s" << std::endl - << "Cutting " << cut_sum << "s" << std::endl - << "Split " << split_sum << "s" << std::endl; -} diff --git a/bench/split-product/formulae.ltl b/bench/split-product/formulae.ltl deleted file mode 100644 index 8cead4155..000000000 --- a/bench/split-product/formulae.ltl +++ /dev/null @@ -1,55 +0,0 @@ -[](!p0) -<>p1 -> (!p0 U p1) -[](p2 -> [](!p0)) -[]((p2 & !p1 & <>p1) -> (!p0 U p1)) -[](p2 & !p1 -> (!p0 U (p1 | []!p0))) -<>(p0) -!p1 U ((p0 & !p1) | []!p1) -[](!p2) | <>(p2 & <>p0) -[](p2 & !p1 -> (!p1 U ((p0 & !p1) | []!p1))) -[](p2 & !p1 -> (!p1 U (p0 & !p1))) -<>p1 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1))))))))) -[]((p2 & <>p1) -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1)))))))))) -[](p2 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U (p1 | []!p0)) | []p0))))))))) -[](p0) -<>p1 -> (p0 U p1) -[](p2 -> [](p0)) -[]((p2 & !p1 & <>p1) -> (p0 U p1)) -[](p2 & !p1 -> (p0 U (p1 | [] p0))) -!p0 U (p3 | []!p0) -<>p1 -> (!p0 U (p3 | p1)) -[]!p2 | <>(p2 & (!p0 U (p3 | []!p0))) -[]((p2 & !p1 & <>p1) -> (!p0 U (p3 | p1))) -[](p2 & !p1 -> (!p0 U ((p3 | p1) | []!p0))) -[](p0 -> <>p3) -<>p1 -> (p0 -> (!p1 U (p3 & !p1))) U p1 -[](p2 -> [](p0 -> <>p3)) -[]((p2 & !p1 & <>p1) -> (p0 -> (!p1 U (p3 & !p1))) U p1) -[](p2 & !p1 -> ((p0 -> (!p1 U (p3 & !p1))) U (p1 | [](p0 -> (!p1 U (p3 & !p1)))))) -<>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4))) -<>p1 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4)))) -([]!p2) | (!p2 U (p2 & <>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4))))) -[]((p2 & <>p1) -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))) -[](p2 -> (<>p0 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4)))))) -(<>(p3 & X<>p4)) -> ((!p3) U p0) -<>p1 -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0)) -([]!p2) | ((!p2) U (p2 & ((<>(p3 & X<>p4)) -> ((!p3) U p0)))) -[]((p2 & <>p1) -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0))) -[](p2 -> (!(p3 & (!p1) & X(!p1 U (p4 & !p1))) U (p1 | p0) | [](!(p3 & X<>p4)))) -[] (p3 & X<> p4 -> X(<>(p4 & <> p0))) -<>p1 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1 -[] (p2 -> [] (p3 & X<> p4 -> X(!p4 U (p4 & <> p0)))) -[] ((p2 & <>p1) -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1) -[] (p2 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U (p1 | [] (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))))) -[] (p0 -> <>(p3 & X<>p4)) -<>p1 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1 -[] (p2 -> [] (p0 -> (p3 & X<> p4))) -[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1) -[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U (p1 | [] (p0 -> (p3 & X<> p4)))) -[] (p0 -> <>(p3 & !p5 & X(!p5 U p4))) -<>p1 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1 -[] (p2 -> [] (p0 -> (p3 & !p5 & X(!p5 U p4)))) -[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1) -[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U (p1 | [] (p0 -> (p3 & !p5 & X(!p5 U p4))))) -!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0) -<>p2 -> (!p2 U (p2 & (!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0)))) \ No newline at end of file diff --git a/bench/split-product/models/cl3serv1.pml b/bench/split-product/models/cl3serv1.pml deleted file mode 100644 index 532408d7e..000000000 --- a/bench/split-product/models/cl3serv1.pml +++ /dev/null @@ -1,43 +0,0 @@ -#define w1 client[0]@wait -#define s1 client[0]@served - -#define C 3 -#define S 1 - -chan clserv = [C] of { int }; -chan servcl = [S] of { int }; - -active [C] proctype client() { - /* the _pid's are: 0 .. C-1 */ - -served: - if - :: (1) -> goto request; - fi; -request: - if - :: (1) -> clserv!_pid; goto wait; - fi; -wait: - if - :: servcl?eval(_pid); goto served; - fi; -} - -active [S] proctype server() { - /* the _pid's are: 0 .. S-1 */ - byte id; - -wait: - if - :: clserv?id -> goto work; - fi; -work: - if - :: (1) -> goto reply; - fi; -reply: - if - :: (1) -> servcl!id; goto wait; - fi; -} diff --git a/bench/split-product/models/cl3serv3.pml b/bench/split-product/models/cl3serv3.pml deleted file mode 100644 index ae2e510b0..000000000 --- a/bench/split-product/models/cl3serv3.pml +++ /dev/null @@ -1,43 +0,0 @@ -#define w1 client[0]@wait -#define s1 client[0]@served - -#define C 3 -#define S 3 - -chan clserv = [C] of { int }; -chan servcl = [S] of { int }; - -active [C] proctype client() { - /* the _pid's are: 0 .. C-1 */ - -served: - if - :: (1) -> goto request; - fi; -request: - if - :: (1) -> clserv!_pid; goto wait; - fi; -wait: - if - :: servcl?eval(_pid); goto served; - fi; -} - -active [S] proctype server() { - /* the _pid's are: 0 .. S-1 */ - byte id; - -wait: - if - :: clserv?id -> goto work; - fi; -work: - if - :: (1) -> goto reply; - fi; -reply: - if - :: (1) -> servcl!id; goto wait; - fi; -} diff --git a/bench/split-product/models/clserv.ltl b/bench/split-product/models/clserv.ltl deleted file mode 100644 index 1ecbfe7fc..000000000 --- a/bench/split-product/models/clserv.ltl +++ /dev/null @@ -1 +0,0 @@ -!([] (w1 -> <> s1)) diff --git a/bench/split-product/models/eeaean.ltl b/bench/split-product/models/eeaean.ltl deleted file mode 100644 index 23666bb82..000000000 --- a/bench/split-product/models/eeaean.ltl +++ /dev/null @@ -1,9 +0,0 @@ -!(<>[](noLeader U zeroLeads)) -!(<>[](noLeader U threeLeads)) -!(<>zeroLeads) -!([]<>zeroLeads) -!(<>threeLeads) -!([](noLeader -> <>zeroLeads)) -!([](noLeader || zeroLeads)) -!((<>[](noLeader || zeroLeads || oneLeads || twoLeads)) && (<>[]((zeroLeads -> (zeroLeads U (noLeader U oneLeads))))) && (<>[]((oneLeads -> (oneLeads U (noLeader U twoLeads))))) && (<>[]((twoLeads -> (twoLeads U (noLeader U zeroLeads)))))) -!((<>[](noLeader || zeroLeads || oneLeads || twoLeads)) && (<>[]((zeroLeads -> (zeroLeads U (noLeader U twoLeads))))) && (<>[]((oneLeads -> (oneLeads U (noLeader U zeroLeads))))) && (<>[]((twoLeads -> (twoLeads U (noLeader U oneLeads)))))) diff --git a/bench/split-product/models/eeaean1.pml b/bench/split-product/models/eeaean1.pml deleted file mode 100644 index 9e58cffd4..000000000 --- a/bench/split-product/models/eeaean1.pml +++ /dev/null @@ -1,116 +0,0 @@ -/* Echo Election Algorithm with Extinction in an Arbitrary Network. */ -/* Variation 1: Node 0 wins every time. */ - -#define L 10 /* size of buffer */ -#define udef 3 - -#define noLeader (nr_leaders == 0) -#define zeroLeads (nr_leaders == 1 && leader == 0) -#define oneLeads (nr_leaders == 1 && leader == 1) -#define twoLeads (nr_leaders == 1 && leader == 2) -#define threeLeads (nr_leaders == 1 && leader == 3) - -mtype = { tok, ldr }; -chan zero_one = [L] of { mtype, byte}; -chan zero_two = [L] of { mtype, byte}; -chan one_zero = [L] of { mtype, byte}; -chan one_two = [L] of { mtype, byte}; -chan two_zero = [L] of { mtype, byte}; -chan two_one = [L] of { mtype, byte}; - -chan nr0 = [0] of {mtype}; -chan nr1 = [0] of {mtype}; -chan nr2 = [0] of {mtype}; - -byte nr_leaders, done, leader; - -inline recvldr () -{ - if - :: lrec == 0 && r != myid -> - out1!ldr(r); - out2!ldr(r); - :: else -> skip; - fi; - lrec++; - win = r; -} - -inline recvtok (q,c) -{ - if - :: r < caw -> - caw = r; - rec = 0; - father = q; - c!tok(r); - :: else -> skip; - fi; - - if - :: r == caw -> - rec++; - if - :: rec == 2 && caw == myid - -> out1!ldr(myid); out2!ldr(myid); - :: rec == 2 && caw != myid && father == neigh1 - -> out1!tok(caw) - :: rec == 2 && caw != myid && father == neigh2 - -> out2!tok(caw) - :: else -> skip; - fi; - :: else -> skip; - fi; -} - -proctype node (chan nr; byte neigh1; chan out1, in1; - byte neigh2; chan out2, in2) -{ byte myid = 3 - neigh1 - neigh2; - byte caw, rec, father, lrec, win, r; - - xr in1; xr in2; - xs out1; xs out2; - -restart: - nr?tok; - caw = myid; rec = 0; lrec = 0; - father = udef; win = udef; r = udef; - - out1!tok(myid); - out2!tok(myid); - do - :: lrec == 2 -> break; - :: in1?ldr(r) -> recvldr(); - :: in2?ldr(r) -> recvldr(); - :: in1?tok(r) -> recvtok(neigh1,out2); - :: in2?tok(r) -> recvtok(neigh2,out1); - od; - - if - :: win == myid -> - leader = myid; - nr_leaders++; - assert(nr_leaders == 1); - :: else -> - skip; - fi; - - done++; - goto restart; -} - -init { - atomic { - run node (nr0,1,zero_one,one_zero,2,zero_two,two_zero); - run node (nr1,0,one_zero,zero_one,2,one_two,two_one); - run node (nr2,0,two_zero,zero_two,1,two_one,one_two); - } - do - :: true -> - done = 0; - nr_leaders = 0; - leader = udef; - nr0!tok; nr1!tok; nr2!tok; - done == 3; - od; -} diff --git a/bench/split-product/models/eeaean2.pml b/bench/split-product/models/eeaean2.pml deleted file mode 100644 index 03828adbe..000000000 --- a/bench/split-product/models/eeaean2.pml +++ /dev/null @@ -1,118 +0,0 @@ -/* Echo Election Algorithm with Extinction in an Arbitrary Network. */ -/* Variation 1: Node 0 wins every time. */ - -#define L 10 /* size of buffer */ -#define udef 3 - -#define noLeader (nr_leaders == 0) -#define zeroLeads (nr_leaders == 1 && leader == 0) -#define oneLeads (nr_leaders == 1 && leader == 1) -#define twoLeads (nr_leaders == 1 && leader == 2) -#define threeLeads (nr_leaders == 1 && leader == 3) - -mtype = { tok, ldr }; -chan zero_one = [L] of { mtype, byte}; -chan zero_two = [L] of { mtype, byte}; -chan one_zero = [L] of { mtype, byte}; -chan one_two = [L] of { mtype, byte}; -chan two_zero = [L] of { mtype, byte}; -chan two_one = [L] of { mtype, byte}; - -chan nr0 = [0] of {mtype, byte}; -chan nr1 = [0] of {mtype, byte}; -chan nr2 = [0] of {mtype, byte}; - -byte nr_leaders, done, leader; - -inline recvldr () -{ - if - :: lrec == 0 && r != myid -> - out1!ldr(r); - out2!ldr(r); - :: else -> skip; - fi; - lrec++; - win = r; -} - -inline recvtok (q,c) -{ - if - :: (r+turn)%3 < (caw+turn)%3 -> - caw = r; - rec = 0; - father = q; - c!tok(r); - :: else -> skip; - fi; - - if - :: r == caw -> - rec++; - if - :: rec == 2 && caw == myid - -> out1!ldr(myid); out2!ldr(myid); - :: rec == 2 && caw != myid && father == neigh1 - -> out1!tok(caw) - :: rec == 2 && caw != myid && father == neigh2 - -> out2!tok(caw) - :: else -> skip; - fi; - :: else -> skip; - fi; -} - -proctype node (chan nr; byte neigh1; chan out1, in1; - byte neigh2; chan out2, in2) -{ byte myid = 3 - neigh1 - neigh2; - byte caw, rec, father, lrec, win, r, turn; - - xr in1; xr in2; - xs out1; xs out2; - -restart: - nr?tok(turn); - caw = myid; rec = 0; lrec = 0; - father = udef; win = udef; r = udef; - - out1!tok(myid); - out2!tok(myid); - do - :: lrec == 2 -> break; - :: in1?ldr(r) -> recvldr(); - :: in2?ldr(r) -> recvldr(); - :: in1?tok(r) -> recvtok(neigh1,out2); - :: in2?tok(r) -> recvtok(neigh2,out1); - od; - - if - :: win == myid -> - leader = myid; - nr_leaders++; - assert(nr_leaders == 1); - :: else -> - skip; - fi; - - done++; - goto restart; -} - -init { - byte turn = 0; - atomic { - run node (nr0,1,zero_one,one_zero,2,zero_two,two_zero); - run node (nr1,0,one_zero,zero_one,2,one_two,two_one); - run node (nr2,0,two_zero,zero_two,1,two_one,one_two); - } - do - :: true -> - done = 0; - nr_leaders = 0; - leader = udef; - nr0!tok(turn); nr1!tok(turn); nr2!tok(turn); - done == 3; - turn = (turn+1)%3; - od; -} diff --git a/bench/split-product/models/formulae.ltl b/bench/split-product/models/formulae.ltl deleted file mode 100644 index 8cead4155..000000000 --- a/bench/split-product/models/formulae.ltl +++ /dev/null @@ -1,55 +0,0 @@ -[](!p0) -<>p1 -> (!p0 U p1) -[](p2 -> [](!p0)) -[]((p2 & !p1 & <>p1) -> (!p0 U p1)) -[](p2 & !p1 -> (!p0 U (p1 | []!p0))) -<>(p0) -!p1 U ((p0 & !p1) | []!p1) -[](!p2) | <>(p2 & <>p0) -[](p2 & !p1 -> (!p1 U ((p0 & !p1) | []!p1))) -[](p2 & !p1 -> (!p1 U (p0 & !p1))) -<>p1 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1))))))))) -[]((p2 & <>p1) -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U p1)))))))))) -[](p2 -> ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | ((!p0 & !p1) U (p1 | ((p0 & !p1) U (p1 | (!p0 U (p1 | []!p0)) | []p0))))))))) -[](p0) -<>p1 -> (p0 U p1) -[](p2 -> [](p0)) -[]((p2 & !p1 & <>p1) -> (p0 U p1)) -[](p2 & !p1 -> (p0 U (p1 | [] p0))) -!p0 U (p3 | []!p0) -<>p1 -> (!p0 U (p3 | p1)) -[]!p2 | <>(p2 & (!p0 U (p3 | []!p0))) -[]((p2 & !p1 & <>p1) -> (!p0 U (p3 | p1))) -[](p2 & !p1 -> (!p0 U ((p3 | p1) | []!p0))) -[](p0 -> <>p3) -<>p1 -> (p0 -> (!p1 U (p3 & !p1))) U p1 -[](p2 -> [](p0 -> <>p3)) -[]((p2 & !p1 & <>p1) -> (p0 -> (!p1 U (p3 & !p1))) U p1) -[](p2 & !p1 -> ((p0 -> (!p1 U (p3 & !p1))) U (p1 | [](p0 -> (!p1 U (p3 & !p1)))))) -<>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4))) -<>p1 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4)))) -([]!p2) | (!p2 U (p2 & <>p0 -> (!p0 U (p3 & !p0 & X(!p0 U p4))))) -[]((p2 & <>p1) -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4))))) -[](p2 -> (<>p0 -> (!p0 U (p1 | (p3 & !p0 & X(!p0 U p4)))))) -(<>(p3 & X<>p4)) -> ((!p3) U p0) -<>p1 -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0)) -([]!p2) | ((!p2) U (p2 & ((<>(p3 & X<>p4)) -> ((!p3) U p0)))) -[]((p2 & <>p1) -> ((!(p3 & (!p1) & X(!p1 U (p4 & !p1)))) U (p1 | p0))) -[](p2 -> (!(p3 & (!p1) & X(!p1 U (p4 & !p1))) U (p1 | p0) | [](!(p3 & X<>p4)))) -[] (p3 & X<> p4 -> X(<>(p4 & <> p0))) -<>p1 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1 -[] (p2 -> [] (p3 & X<> p4 -> X(!p4 U (p4 & <> p0)))) -[] ((p2 & <>p1) -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U p1) -[] (p2 -> (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))) U (p1 | [] (p3 & X(!p1 U p4) -> X(!p1 U (p4 & <> p0))))) -[] (p0 -> <>(p3 & X<>p4)) -<>p1 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1 -[] (p2 -> [] (p0 -> (p3 & X<> p4))) -[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U p1) -[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & X(!p1 U p4)))) U (p1 | [] (p0 -> (p3 & X<> p4)))) -[] (p0 -> <>(p3 & !p5 & X(!p5 U p4))) -<>p1 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1 -[] (p2 -> [] (p0 -> (p3 & !p5 & X(!p5 U p4)))) -[] ((p2 & <>p1) -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U p1) -[] (p2 -> (p0 -> (!p1 U (p3 & !p1 & !p5 & X((!p1 & !p5) U p4)))) U (p1 | [] (p0 -> (p3 & !p5 & X(!p5 U p4))))) -!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0) -<>p2 -> (!p2 U (p2 & (!p0 U ((p0 U ((!p0 U ((p0 U ([]!p0 | []p0)) | []!p0)) | []!p0)) | []!p0)))) \ No newline at end of file diff --git a/bench/split-product/models/leader.ltl b/bench/split-product/models/leader.ltl deleted file mode 100644 index 0c2217f4f..000000000 --- a/bench/split-product/models/leader.ltl +++ /dev/null @@ -1 +0,0 @@ -!(<>[]oneLeader) \ No newline at end of file diff --git a/bench/split-product/models/leader.pml b/bench/split-product/models/leader.pml deleted file mode 100644 index cf7a1300b..000000000 --- a/bench/split-product/models/leader.pml +++ /dev/null @@ -1,89 +0,0 @@ -/* Dolev, Klawe & Rodeh for leader election in unidirectional ring - * `An O(n log n) unidirectional distributed algorithm for extrema - * finding in a circle,' J. of Algs, Vol 3. (1982), pp. 245-260 - */ - -#define elected (nr_leaders > 0) -#define noLeader (nr_leaders == 0) -#define oneLeader (nr_leaders == 1) - -#define N 5 /* nr of processes (use 5 for demos) */ -#define I 3 /* node given the smallest number */ -#define L 10 /* size of buffer (>= 2*N) */ - -mtype = { one, two, winner }; -chan q[N] = [L] of { mtype, byte}; - -byte nr_leaders = 0; - -proctype node (chan in, out; byte mynumber) -{ bit Active = 1, know_winner = 0; - byte nr, maximum = mynumber, neighbourR; - - xr in; - xs out; - - printf("MSC: %d\n", mynumber); - out!one(mynumber); -end: do - :: in?one(nr) -> - if - :: Active -> - if - :: nr != maximum -> - out!two(nr); - neighbourR = nr - :: else -> - /* Raynal p.39: max is greatest number */ - assert(nr == N); - know_winner = 1; - out!winner,nr; - fi - :: else -> - out!one(nr) - fi - - :: in?two(nr) -> - if - :: Active -> - if - :: neighbourR > nr && neighbourR > maximum -> - maximum = neighbourR; - out!one(neighbourR) - :: else -> - Active = 0 - fi - :: else -> - out!two(nr) - fi - :: in?winner,nr -> - if - :: nr != mynumber -> - printf("MSC: LOST\n"); - :: else -> - printf("MSC: LEADER\n"); - nr_leaders++; - assert(nr_leaders == 1) - fi; - if - :: know_winner - :: else -> out!winner,nr - fi; - break - od -} - -init { - byte proc; - atomic { - proc = 1; - do - :: proc <= N -> - run node (q[proc-1], q[proc%N], (N+I-proc)%N+1); - proc++ - :: proc > N -> - break - od - } -} - diff --git a/bench/split-product/models/mobile1.ltl b/bench/split-product/models/mobile1.ltl deleted file mode 100644 index 7ed106308..000000000 --- a/bench/split-product/models/mobile1.ltl +++ /dev/null @@ -1,2 +0,0 @@ -!((![]<>(r)) -> [](<>p -> <>q)) - diff --git a/bench/split-product/models/mobile1.pml b/bench/split-product/models/mobile1.pml deleted file mode 100644 index 05c1c21b8..000000000 --- a/bench/split-product/models/mobile1.pml +++ /dev/null @@ -1,155 +0,0 @@ -/* - * Model of cell-phone handoff strategy in a mobile network. - * A translation from the pi-calculus description of this - * model presented in: - * Fredrik Orava and Joachim Parrow, 'An algebraic verification - * of a mobile network,' Formal aspects of computing, 4:497-543 (1992). - * For more information on this model, email: joachim@it.kth.se - * - * See also the simplified version of this model in mobile2 - * - * The ltl property definition for this version is in mobile1.ltl - * - * to perform the verification with xspin, simply use the ltl property - * manager, which will load the above .ltl file by default. - * to perform the verificaion from a Unix command line, type: - * $ spin -a -N mobile1.ltl mobile1 - * $ cc -o pan pan.c - * $ pan -a - */ - -#define p in?[red] -#define q out?[red] -#define r (BS[a_id]@progress || BS[p_id]@progress) - -mtype = { data, ho_cmd, ho_com, ho_acc, ho_fail, ch_rel, white, red, blue }; - -chan in = [1] of { mtype }; -chan out = [1] of { mtype }; - -byte a_id, p_id; /* ids of processes refered to in the property */ - -proctype CC(chan fa, fp, l) /* communication controller */ -{ chan m_old, m_new, x; - mtype v; - - do - :: in?v -> - printf("MSC: DATA\n"); - fa!data; fa!v - :: l?m_new -> - fa!ho_cmd; fa!m_new; - printf("MSC: HAND-OFF\n"); - if - :: fp?ho_com -> - printf("MSC: CH_REL\n"); - fa!ch_rel; fa?m_old; - l!m_old; - x = fa; fa = fp; fp = x - :: fa?ho_fail -> - printf("MSC: FAIL\n"); - l!m_new - fi - od -} - -proctype HC(chan l, m) /* handover controller */ -{ - do - :: l!m; l?m - od -} - -proctype MSC(chan fa, fp, m) /* mobile switching center */ -{ chan l = [0] of { chan }; - - atomic { - run HC(l, m); - run CC(fa, fp, l) - } -} - -proctype BS(chan f, m; bit how) /* base station */ -{ chan v; - - if - :: how -> goto Active - :: else -> goto Passive - fi; - -Active: - printf("MSC: ACTIVE\n"); - do - :: f?data -> f?v; m!data; m!v - :: f?ho_cmd -> /* handover command */ -progress: f?v; m!ho_cmd; m!v; - if - :: f?ch_rel -> - f!m; - goto Passive - :: m?ho_fail -> - printf("MSC: FAILURE\n"); - f!ho_fail - fi - od; - -Passive: - printf("MSC: PASSIVE\n"); - m?ho_acc -> f!ho_com; - goto Active -} - -proctype MS(chan m) /* mobile station */ -{ chan m_new; - mtype v; - - do - :: m?data -> m?v; out!v - :: m?ho_cmd; m?m_new; - if - :: m_new!ho_acc; m = m_new - :: m!ho_fail - fi - od -} - -proctype P(chan fa, fp) -{ chan m = [0] of { mtype }; - - atomic { - run MSC(fa, fp, m); - p_id = run BS(fp, m, 0) /* passive base station */ - } -} - -proctype Q(chan fa) -{ chan m = [0] of { mtype }; /* mixed use as mtype/chan */ - - atomic { - a_id = run BS(fa, m, 1); /* active base station */ - run MS(m) - } -} - -active proctype System() -{ chan fa = [0] of { mtype }; /* mixed use as mtype/chan */ - chan fp = [0] of { mtype }; /* mixed use as mtype/chan */ - - atomic { - run P(fa, fp); - run Q(fa) - } -} - -active proctype top() -{ - do - :: in!red; in!white; in!blue - od -} -active proctype bot() -{ - do /* deadlock on loss or duplication */ - :: out?red; out?white; out?blue - od -} diff --git a/bench/split-product/models/mobile2.ltl b/bench/split-product/models/mobile2.ltl deleted file mode 100644 index b450332dc..000000000 --- a/bench/split-product/models/mobile2.ltl +++ /dev/null @@ -1 +0,0 @@ -!((![]<>(r)) -> [](<>p -> <>q)) \ No newline at end of file diff --git a/bench/split-product/models/mobile2.pml b/bench/split-product/models/mobile2.pml deleted file mode 100644 index 21ad0c62a..000000000 --- a/bench/split-product/models/mobile2.pml +++ /dev/null @@ -1,136 +0,0 @@ -/* - * Simplified model of cell-phone handoff strategy in a mobile network. - * A translation from the pi-calculus description of this - * model presented in: - * Fredrik Orava and Joachim Parrow, 'An algebraic verification - * of a mobile network,' Formal aspects of computing, 4:497-543 (1992). - * For more information on this model, email: joachim@it.kth.se - * - * This version exploits some Promela features to reduce the number - * of processes -- which looks better in simulations, and reduces - * complexity (by about 60%) in verification. - * - * See also the more literal version of this model in mobile1. - * - * The ltl property definition for this version is in mobile2.ltl - * - * to perform the verification with xspin, simply use the ltl property - * manager, which will load the above .ltl file by default. - * to perform the verificaion from a Unix command line, type: - * $ spin -a -N mobile2.ltl mobile2 - * $ cc -o pan pan.c - * $ pan -a - */ - -#define p in?[red] -#define q out?[red] -#define r (BS[a_id]@progress || BS[p_id]@progress) - -mtype = { data, ho_cmd, ho_com, ho_acc, ho_fail, ch_rel, white, red, blue }; - -chan in = [1] of { mtype }; -chan out = [1] of { mtype }; -chan fa = [0] of { chan }; -chan fp = [0] of { chan }; -chan m1 = [0] of { chan }; -chan m2 = [0] of { chan }; -chan l = [0] of { chan }; - -byte a_id, p_id; /* ids of processes refered to in the property */ - -proctype CC() /* communication controller */ -{ chan m_old, m_new, x; - mtype v; - - do - :: in?v -> - printf("MSC: DATA\n"); - fa!data; fa!v - :: l?m_new -> - fa!ho_cmd; fa!m_new; - printf("MSC: HAND-OFF\n"); - if - :: fp?ho_com -> - printf("MSC: CH_REL\n"); - fa!ch_rel; fa?m_old; - l!m_old; - x = fa; fa = fp; fp = x - :: fa?ho_fail -> - printf("MSC: FAIL\n"); - l!m_new - fi - od -} - -proctype HC(chan m) /* handover controller */ -{ - do - :: l!m; l?m - od -} - -proctype BS(chan f, m; bit how) /* base station */ -{ chan v; - - if - :: how -> goto Active - :: else -> goto Passive - fi; - -Active: - printf("MSC: ACTIVE\n"); - do - :: f?data -> f?v; m!data; m!v - :: f?ho_cmd -> /* handover command */ -progress: f?v; m!ho_cmd; m!v; - if - :: f?ch_rel -> - f!m; - goto Passive - :: m?ho_fail -> - printf("MSC: FAILURE\n"); - f!ho_fail - fi - od; - -Passive: - printf("MSC: PASSIVE\n"); - m?ho_acc -> f!ho_com; - goto Active -} - -proctype MS(chan m) /* mobile station */ -{ chan m_new; - mtype v; - - do - :: m?data -> m?v; out!v - :: m?ho_cmd; m?m_new; - if - :: m_new!ho_acc; m = m_new - :: m!ho_fail - fi - od -} - -active proctype System() -{ - atomic { - run HC(m1); - run CC(); - p_id = run BS(fp, m1, 0); /* passive base station */ - a_id = run BS(fa, m2, 1); /* active base station */ - run MS(m2) - } - -end: do - :: in!red; in!white; in!blue - od -} - -active proctype Out() -{ -end: do /* deadlocks if order is disturbed */ - :: out?red; out?white; out?blue - od -} diff --git a/bench/split-product/models/zune.ltl b/bench/split-product/models/zune.ltl deleted file mode 100644 index 1606747c7..000000000 --- a/bench/split-product/models/zune.ltl +++ /dev/null @@ -1 +0,0 @@ -![] (zune_at_S -> <> zune_at_E) \ No newline at end of file diff --git a/bench/split-product/models/zune.pml b/bench/split-product/models/zune.pml deleted file mode 100644 index 123220fb0..000000000 --- a/bench/split-product/models/zune.pml +++ /dev/null @@ -1,70 +0,0 @@ -/* - * input: days elapsed since Jan 1, 1980 - * intended output: year and daynr in current year - * - * a bug caused all Zune-30 players to freeze on Dec 31, 2008 - * http://www.zuneboards.com/forums/zune-news/38143-cause-zune-30-leapyear-problem-isolated.html - * - * Wikepedia: - * The bug was in the firmware clock-driver, which was written by Freescale - * for their MC13783 PMIC processor. The same bug froze up Toshiba Gigabeat S - * media players that share the same hardware and driver. - */ - -#define IsLeapYear(y) (((y%4 == 0) && (y%100 != 0)) || (y%400 == 0)) - -chan q = [0] of { short }; - -active proctype zune() -{ short year = 1980; - short days; - -end: do - :: q?days -> -S: do - :: days > 365 -> - if - :: IsLeapYear(year) -> - if - :: days > 366 -> - days = days - 366; - year++ - :: else -#ifdef FIX - -> break -#endif - fi - :: else -> - days = days - 365; - year++ - fi - :: else -> - break - od; -E: printf("Year: %d, Day %d\n", year, days) - od; - /* check that the date is in a valid range */ - assert(days >= 1 && days <= 366); - assert(days < 366 || IsLeapYear(year)) -} - -init { - /* jan 1, 2008 */ - short days = (2008 - 1980) * 365 + (2008-1980)/4; - - if - :: q!days + 365 - :: q!days + 366 - :: q!days + 367 - fi -} - -#define zune_at_S zune@S -#define zune_at_E zune@E - -/* sample analysis: - spin -a zune.pml - cc -o pan pan.c - ./pan -a # find matches of formula - spin -t -p -l zune.pml # replay error sequence - */ diff --git a/bench/split-product/pml2tgba.pl b/bench/split-product/pml2tgba.pl deleted file mode 100755 index fef5294e4..000000000 --- a/bench/split-product/pml2tgba.pl +++ /dev/null @@ -1,227 +0,0 @@ -#!/usr/bin/perl -w -# -# Copyright (C) 2004 Stefan Schwoon -# -# This program is free software; you can redistribute it and/or modify -# it under the terms of the GNU General Public License as published by -# the Free Software Foundation; either version 3 of the License, or -# (at your option) any later version. -# -# This program is distributed in the hope that it will be useful, -# but WITHOUT ANY WARRANTY; without even the implied warranty of -# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the -# GNU General Public License for more details. -# -# You should have received a copy of the GNU General Public License -# along with this program. If not, see .# -# -# 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 <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 () -{ - last if /^proctype :never/; -} -while () -{ - 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 () { - last if (/ New state 0/); -} -my %acc = (); -push @stack, [$dfsstate, $buechitrans, %acc]; - -my %allaccs = (); -my %trans_list; -my $prop = "BUG"; -while () { - 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: diff --git a/configure.ac b/configure.ac index ab45c12be..5973f62e8 100644 --- a/configure.ac +++ b/configure.ac @@ -162,8 +162,6 @@ AC_CONFIG_FILES([ bench/ltlclasses/Makefile bench/ltl2tgba/Makefile bench/ltl2tgba/defs - bench/scc-stats/Makefile - bench/split-product/Makefile bench/spin13/Makefile bench/wdba/Makefile doc/Doxyfile diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 7aa6f6da0..cc2816999 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -31,7 +31,6 @@ tgbaalgos_HEADERS = \ bfssteps.hh \ complete.hh \ compsusp.hh \ - cutscc.hh \ cycles.hh \ dtgbacomp.hh \ degen.hh \ @@ -79,7 +78,6 @@ libtgbaalgos_la_SOURCES = \ bfssteps.cc \ complete.cc \ compsusp.cc \ - cutscc.cc \ cycles.cc \ dtgbacomp.cc \ degen.cc \ diff --git a/src/tgbaalgos/cutscc.cc b/src/tgbaalgos/cutscc.cc deleted file mode 100644 index 417491682..000000000 --- a/src/tgbaalgos/cutscc.cc +++ /dev/null @@ -1,385 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2011, 2012, 2013, 2014 Laboratoire de Recherche -// et Developpement de l'Epita (LRDE). -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - -#include -#include -#include -#include -#include "tgba/tgbaexplicit.hh" -#include "cutscc.hh" - -namespace spot -{ - namespace - { - static tgba* - cut_scc(const tgba* a, const scc_map& m, - const std::set& s) - { - tgba_explicit_string* sub_a = new tgba_explicit_string(a->get_dict()); - const state* cur = a->get_init_state(); - std::queue tovisit; - // Setup - state_unicity_table seen; - unsigned scc_number; - std::string cur_format = a->format_state(cur); - std::set::iterator it; - // Check if we have at least one accepting SCC. - for (it = s.begin(); it != s.end() && !m.accepting(*it); ++it) - continue; - assert(it != s.end()); - tovisit.push(seen(cur)); - sub_a->add_state(cur_format); - sub_a->copy_acceptance_conditions_of(a); - // If the initial is not part of one of the desired SCC, exit - assert(s.find(m.scc_of_state(cur)) != s.end()); - - // Perform BFS to visit each state. - while (!tovisit.empty()) - { - cur = tovisit.front(); - tovisit.pop(); - for (auto sit: a->succ(cur)) - { - cur_format = a->format_state(cur); - state* dst = sit->current_state(); - std::string dst_format = a->format_state(dst); - scc_number= m.scc_of_state(dst); - // Is the successor included in one of the desired SCC ? - if (s.find(scc_number) != s.end()) - { - if (seen.is_new(dst)) - tovisit.push(dst); - state_explicit_string::transition* t = - sub_a->create_transition(cur_format, dst_format); - sub_a->add_conditions(t, sit->current_condition()); - bdd acc = sit->current_acceptance_conditions(); - sub_a->add_acceptance_conditions(t, acc); - } - else - { - dst->destroy(); - } - } - } - return sub_a; - } - - static unsigned set_distance(const sccs_set* s1, - const sccs_set* s2, - const std::vector& scc_sizes) - { - // Compute the distance between two sets. - // Formula is : distance = size(s1) + size(s2) - size(s1 inter s2) - std::set::iterator it; - std::set result; - unsigned inter_sum = 0; - std::set_intersection(s1->sccs.begin(), s1->sccs.end(), - s2->sccs.begin(), s2->sccs.end(), - std::inserter(result, result.begin())); - for (it = result.begin(); it != result.end(); ++it) - inter_sum += scc_sizes[*it]; - return s1->size + s2->size - 2*inter_sum; - } - - static sccs_set* set_union(sccs_set* s1, - sccs_set* s2, - const std::vector& 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::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 seen; - std::vector >* rec_paths; - }; - - static void find_paths_sub(unsigned init_scc, - const scc_map& m, - recurse_data& d, - const std::vector& 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 it_stack; - std::stack scc_stack; - std::vector 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 >* 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::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 >* 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 >; - for (i = 0; i < scc_count; i++) - { - std::vector list_set; - d.rec_paths->push_back(list_set); - } - // We use a vector to recall the size of all SCCs. - std::vector scc_sizes(scc_count, 0); - for (i = 0; i < scc_count; ++i) - scc_sizes[i] = m.states_of(i).size(); - state* initial_state = a->get_init_state(); - unsigned init = m.scc_of_state(initial_state); - initial_state->destroy(); - // Find all interesting pathes in our automaton. - find_paths_sub(init, m, d, scc_sizes); - - return d.rec_paths; - } - - std::list 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 >* rec_paths = find_paths(a, m); - state* initial_state = a->get_init_state(); - unsigned init = m.scc_of_state(initial_state); - initial_state->destroy(); - std::vector* final_sets =&(*rec_paths)[init]; - if (rec_paths->empty()) - { - std::list empty; - return empty; - } - - unsigned paths_count = final_sets->size(); - std::vector< std::vector > dist; - for (i = 0; i < paths_count; ++i) - { - std::vector dist_sub(i, 0); - dist.push_back(dist_sub); - } - - // We use a vector to recall the size of all SCCs. - std::vector 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 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 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* paths, scc_map& m) - { - unsigned scc_count = m.scc_count(); - std::vector sccs_marked (scc_count, false); - std::vector 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* cur_path = &(*paths)[i]->sccs; - std::set::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* cur_path = &(*paths)[max_index]->sccs; - std::set::iterator it; - for (it = cur_path->begin(); it != cur_path->end(); ++it) - { - sccs_marked[*it] = true; - } - } - return iter_count; - } -} diff --git a/src/tgbaalgos/cutscc.hh b/src/tgbaalgos/cutscc.hh deleted file mode 100644 index c12e60a6a..000000000 --- a/src/tgbaalgos/cutscc.hh +++ /dev/null @@ -1,48 +0,0 @@ -// -*- coding: utf-8 -*- -// Copyright (C) 2009, 2013 Laboratoire de Recherche et Developpement de -// l'Epita (LRDE). -// -// This file is part of Spot, a model checking library. -// -// Spot is free software; you can redistribute it and/or modify it -// under the terms of the GNU General Public License as published by -// the Free Software Foundation; either version 3 of the License, or -// (at your option) any later version. -// -// Spot is distributed in the hope that it will be useful, but WITHOUT -// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY -// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public -// License for more details. -// -// You should have received a copy of the GNU General Public License -// along with this program. If not, see . - - -#ifndef SPOT_TGBAALGOS_CUTSCC_HH -# define SPOT_TGBAALGOS_CUTSCC_HH - -#include -#include -#include "tgba/tgba.hh" -#include "tgbaalgos/scc.hh" - -namespace spot -{ - struct sccs_set - { - std::set sccs; - unsigned size; - }; - - SPOT_API std::vector >* - find_paths(tgba* a, const scc_map& m); - - SPOT_API unsigned - max_spanning_paths(std::vector* paths, scc_map& m); - - SPOT_API std::list - split_tgba(tgba* a, const scc_map& m, unsigned split_number); - -} - -#endif // SPOT_TGBAALGOS_CUTSCC_HH