diff --git a/ChangeLog b/ChangeLog index 4ae76de91..9bd7f940d 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,9 +1,30 @@ +2009-07-08 Félix Abecassis + + 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 * src/tgba/tgbacomplement.cc: Fix the transformation from Streett to TGBA. * src/tgbatest/complementation.test: Modify tests. - + 2009-06-17 Alexandre Duret-Lutz * bench/emptchk/pml2tgba.pl: Adjust to work with Spin 5.2.0. diff --git a/bench/Makefile.am b/bench/Makefile.am index 939b98804..23e86fa82 100644 --- a/bench/Makefile.am +++ b/bench/Makefile.am @@ -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 diff --git a/bench/scc-stats/Makefile.am b/bench/scc-stats/Makefile.am new file mode 100644 index 000000000..eb66643f0 --- /dev/null +++ b/bench/scc-stats/Makefile.am @@ -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 diff --git a/bench/scc-stats/README b/bench/scc-stats/README new file mode 100644 index 000000000..535552536 --- /dev/null +++ b/bench/scc-stats/README @@ -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 \ No newline at end of file diff --git a/bench/scc-stats/formulae.ltl b/bench/scc-stats/formulae.ltl new file mode 100644 index 000000000..8cead4155 --- /dev/null +++ b/bench/scc-stats/formulae.ltl @@ -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)))) \ No newline at end of file diff --git a/bench/scc-stats/stats.cc b/bench/scc-stats/stats.cc new file mode 100644 index 000000000..024ce7680 --- /dev/null +++ b/bench/scc-stats/stats.cc @@ -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 +#include +#include "tgbaalgos/scc.hh" +#include "tgbaalgos/cutscc.hh" +#include "tgba/tgbafromfile.hh" + +namespace spot +{ + unsigned tgba_size(const tgba* a) + { + typedef Sgi::hash_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. + 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& 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 acc_scc; + std::vector dead_scc; + std::vector acc_paths; + std::vector dead_paths; + std::vector spanning_paths; + std::vector 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 >* 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; +} diff --git a/bench/split-product/Makefile.am b/bench/split-product/Makefile.am new file mode 100644 index 000000000..cb78dcf01 --- /dev/null +++ b/bench/split-product/Makefile.am @@ -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 \ No newline at end of file diff --git a/bench/split-product/README b/bench/split-product/README new file mode 100644 index 000000000..0718617f6 --- /dev/null +++ b/bench/split-product/README @@ -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/ + + 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 new file mode 100644 index 000000000..46aef34c2 --- /dev/null +++ b/bench/split-product/cutscc.cc @@ -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 +#include +#include +#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 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. + 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 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 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; + 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; +} diff --git a/bench/split-product/formulae.ltl b/bench/split-product/formulae.ltl new file mode 100644 index 000000000..8cead4155 --- /dev/null +++ b/bench/split-product/formulae.ltl @@ -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)))) \ No newline at end of file diff --git a/bench/split-product/models/cl3serv1.pml b/bench/split-product/models/cl3serv1.pml new file mode 100644 index 000000000..532408d7e --- /dev/null +++ b/bench/split-product/models/cl3serv1.pml @@ -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; +} diff --git a/bench/split-product/models/cl3serv3.pml b/bench/split-product/models/cl3serv3.pml new file mode 100644 index 000000000..ae2e510b0 --- /dev/null +++ b/bench/split-product/models/cl3serv3.pml @@ -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; +} diff --git a/bench/split-product/models/clserv.ltl b/bench/split-product/models/clserv.ltl new file mode 100644 index 000000000..1ecbfe7fc --- /dev/null +++ b/bench/split-product/models/clserv.ltl @@ -0,0 +1 @@ +!([] (w1 -> <> s1)) diff --git a/bench/split-product/models/eeaean.ltl b/bench/split-product/models/eeaean.ltl new file mode 100644 index 000000000..23666bb82 --- /dev/null +++ b/bench/split-product/models/eeaean.ltl @@ -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)))))) diff --git a/bench/split-product/models/eeaean1.pml b/bench/split-product/models/eeaean1.pml new file mode 100644 index 000000000..9e58cffd4 --- /dev/null +++ b/bench/split-product/models/eeaean1.pml @@ -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; +} diff --git a/bench/split-product/models/eeaean2.pml b/bench/split-product/models/eeaean2.pml new file mode 100644 index 000000000..03828adbe --- /dev/null +++ b/bench/split-product/models/eeaean2.pml @@ -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; +} diff --git a/bench/split-product/models/formulae.ltl b/bench/split-product/models/formulae.ltl new file mode 100644 index 000000000..8cead4155 --- /dev/null +++ b/bench/split-product/models/formulae.ltl @@ -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)))) \ No newline at end of file diff --git a/bench/split-product/models/leader.ltl b/bench/split-product/models/leader.ltl new file mode 100644 index 000000000..0c2217f4f --- /dev/null +++ b/bench/split-product/models/leader.ltl @@ -0,0 +1 @@ +!(<>[]oneLeader) \ No newline at end of file diff --git a/bench/split-product/models/leader.pml b/bench/split-product/models/leader.pml new file mode 100644 index 000000000..cf7a1300b --- /dev/null +++ b/bench/split-product/models/leader.pml @@ -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 + } +} + diff --git a/bench/split-product/models/mobile1.ltl b/bench/split-product/models/mobile1.ltl new file mode 100644 index 000000000..7ed106308 --- /dev/null +++ b/bench/split-product/models/mobile1.ltl @@ -0,0 +1,2 @@ +!((![]<>(r)) -> [](<>p -> <>q)) + diff --git a/bench/split-product/models/mobile1.pml b/bench/split-product/models/mobile1.pml new file mode 100644 index 000000000..05c1c21b8 --- /dev/null +++ b/bench/split-product/models/mobile1.pml @@ -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 +} diff --git a/bench/split-product/models/mobile2.ltl b/bench/split-product/models/mobile2.ltl new file mode 100644 index 000000000..b450332dc --- /dev/null +++ b/bench/split-product/models/mobile2.ltl @@ -0,0 +1 @@ +!((![]<>(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 new file mode 100644 index 000000000..21ad0c62a --- /dev/null +++ b/bench/split-product/models/mobile2.pml @@ -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 +} diff --git a/bench/split-product/models/zune.ltl b/bench/split-product/models/zune.ltl new file mode 100644 index 000000000..1606747c7 --- /dev/null +++ b/bench/split-product/models/zune.ltl @@ -0,0 +1 @@ +![] (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 new file mode 100644 index 000000000..123220fb0 --- /dev/null +++ b/bench/split-product/models/zune.pml @@ -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 + */ diff --git a/bench/split-product/pml2tgba.pl b/bench/split-product/pml2tgba.pl new file mode 100755 index 000000000..4fdd76c39 --- /dev/null +++ b/bench/split-product/pml2tgba.pl @@ -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 <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 f1f9bada8..9415c08c4 100644 --- a/configure.ac +++ b/configure.ac @@ -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 diff --git a/src/tgba/Makefile.am b/src/tgba/Makefile.am index 624f2f031..dd825e136 100644 --- a/src/tgba/Makefile.am +++ b/src/tgba/Makefile.am @@ -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 diff --git a/src/tgba/tgbafromfile.cc b/src/tgba/tgbafromfile.cc new file mode 100644 index 000000000..1288c2f88 --- /dev/null +++ b/src/tgba/tgbafromfile.cc @@ -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_; + } +} + diff --git a/src/tgba/tgbafromfile.hh b/src/tgba/tgbafromfile.hh new file mode 100644 index 000000000..fd48a1f48 --- /dev/null +++ b/src/tgba/tgbafromfile.hh @@ -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 +#include +#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 diff --git a/src/tgbaalgos/Makefile.am b/src/tgbaalgos/Makefile.am index 0e8d6dd06..56436b273 100644 --- a/src/tgbaalgos/Makefile.am +++ b/src/tgbaalgos/Makefile.am @@ -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 \ diff --git a/src/tgbaalgos/cutscc.cc b/src/tgbaalgos/cutscc.cc new file mode 100644 index 000000000..3cd2dcaf0 --- /dev/null +++ b/src/tgbaalgos/cutscc.cc @@ -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 +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#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* s) + { + tgba_explicit* sub_a = new tgba_explicit(a->get_dict()); + state* cur = a->get_init_state(); + std::queue tovisit; + typedef Sgi::hash_set hash_type; + // Setup + hash_type 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(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::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& 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; + } + + 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; + }; + + 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); + delete initial_state; + // 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); + delete initial_state; + 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 new file mode 100644 index 000000000..88f0528b0 --- /dev/null +++ b/src/tgbaalgos/cutscc.hh @@ -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 +#include +#include +#include "tgba/public.hh" +#include "tgbaalgos/scc.hh" + +namespace spot +{ + struct sccs_set + { + std::set sccs; + unsigned size; + }; + + std::vector >* find_paths(tgba* a, const scc_map& m); + unsigned max_spanning_paths(std::vector* paths, scc_map& m); + std::list split_tgba(tgba* a, const scc_map& m, + unsigned split_number); + +} + +#endif // SPOT_TGBAALGOS_CUTSCC_HH diff --git a/src/tgbaalgos/scc.cc b/src/tgbaalgos/scc.cc index 5af363198..21969d38e 100644 --- a/src/tgbaalgos/scc.cc +++ b/src/tgbaalgos/scc.cc @@ -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& 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; diff --git a/src/tgbaalgos/scc.hh b/src/tgbaalgos/scc.hh index 38098b79a..9eb85071d 100644 --- a/src/tgbaalgos/scc.hh +++ b/src/tgbaalgos/scc.hh @@ -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);