diff --git a/README.md b/README.md index 99a2618608cdf71894cdea0a17c700924c4f9140..6615ad464b78aa3bc2364aed1d26227ec35e541e 100644 --- a/README.md +++ b/README.md @@ -1,53 +1,47 @@ -<<<<<<< README.md -# Tool for Symbolic Observation Graph-Based Generation of Test Paths -From the description of Petri net, this code is able to generate the observable paths then the abstract paths. +# Symbolic Observation Graph-Based Generation of Test Paths ---- REQUIREMENTS ---------------------------------------------------- ---------------------------------------------------------------------- +`sog-test-paths` generates the observable paths from a Petri net model. It also +generates the abstract paths. -* A C++ compiler (gcc version 9.3.0). +## Requirements ---- USE ----------------------------------------------------------- ---------------------------------------------------------------------- +- A C++ compiler (`gcc >= 9.3.0`). -To compile this collection of code you have to: +## Use --First,run the "make" command inside of the directory "buddy22". This will create/update the library libbdd.a this directory includes the library of Binary Decision Diagrams. +To compile the tool you have to: --Second, run "make" in the "parser" directory, this directory is responsible for the creation of the Petri net from its description file "file.net". +- First, run the `make` command inside the directory `buddy22`. This will + create/update the library libbdd.a this directory includes the library of Binary + Decision Diagrams. --Then, you run the "make" command in the main directory to generate the executable file "StructAnalysis". +-Second, run "make" in the "parser" directory, this directory is responsible for the creation of the Petri net from its description file "file.net". --To run this executable on any example, we have to access the main directory and execute the command "./StructAnalysis ./Samples/file.net" for the paper we used the example file Samples/exemple.net. +-Then, you run the "make" command in the main directory to generate the executable file "StructAnalysis". +-To run this executable on any example, we have to access the main directory and execute the command "./StructAnalysis ./Samples/file.net" for the paper we used the example file Samples/exemple.net. ---- Exemple ------------------------------------------ ------------------------------------------------------- +## --- Exemple ------------------------------------------ We treat the exemple of 2 dining philosophers. The figure bellow represents the Petri Net corresponding to 2 philosophers. + <p align="center"> <img src="philo2.png" width="350" alt="petri net"> </p> - - *Step1: Extract the set of unobservable transitions using the pattern. For this exemple Unobs={GoEat0, GoLeft0, GoRight0, GoEat1, GoLeft1, GoRight1}.<br /> - *Step2: Deduce the set of observable transitions. Obs={Release0, Release1}.<br /> - *Step3: Build the SOG (Symbolic Observation Graph) starting from the Petri Net and the set of observable transitions and build the observable paths on the fly. We get the set of observed paths {\<Release0\>,\<Release1\>}. <br /> - *Step4: Complete the Observable paths by unobservable transitions by making backtracking in each aggregate. - The final result for this example is the set of abstract paths (complete paths): {\<GoEat0 GoRight0 GoLeft0 Release0\>,\<GoEat1 GoRight1 GoLeft1 GoEat0 Release1\>} +*Step1: Extract the set of unobservable transitions using the pattern. For this exemple Unobs={GoEat0, GoLeft0, GoRight0, GoEat1, GoLeft1, GoRight1}.<br /> +*Step2: Deduce the set of observable transitions. Obs={Release0, Release1}.<br /> +*Step3: Build the SOG (Symbolic Observation Graph) starting from the Petri Net and the set of observable transitions and build the observable paths on the fly. We get the set of observed paths {\<Release0\>,\<Release1\>}. <br /> +*Step4: Complete the Observable paths by unobservable transitions by making backtracking in each aggregate. +The final result for this example is the set of abstract paths (complete paths): {\<GoEat0 GoRight0 GoLeft0 Release0\>,\<GoEat1 GoRight1 GoLeft1 GoEat0 Release1\>} - -----Experimental result ---------------------------- ----------------------------------------------------- +## ----Experimental result ---------------------------- We have applied our approach to the Dining philosophers problem by varying the number of philosophers each time (2,3...100 philosophers). We evaluate the size of the reachability graph, the number of observed transitions , the number of aggregates found by applying our tool and calculate the execution time for each example. We notice that the size of the reachability graph is increasing exponentially. The results are summarised in the attached table. + <p align="center"> <img src="comparatif.png" width="600" alt="comparative table"> </p> - - - - diff --git a/buddy22/src/bddio.o b/buddy22/src/bddio.o deleted file mode 100644 index c87b58d665872f2c8bf6a6eacf16e08a0de940ad..0000000000000000000000000000000000000000 Binary files a/buddy22/src/bddio.o and /dev/null differ diff --git a/buddy22/src/bddop.o b/buddy22/src/bddop.o deleted file mode 100644 index 3e6bbaf2e2d8c6fca26c64b8e8ce250ee73120af..0000000000000000000000000000000000000000 Binary files a/buddy22/src/bddop.o and /dev/null differ diff --git a/buddy22/src/bvec.o b/buddy22/src/bvec.o deleted file mode 100644 index 45967f044a081308260c8242bb9f3c88910043ac..0000000000000000000000000000000000000000 Binary files a/buddy22/src/bvec.o and /dev/null differ diff --git a/buddy22/src/cache.o b/buddy22/src/cache.o deleted file mode 100644 index 0165d4e5e3a7082f9f8ac0830fe8c603e513d09e..0000000000000000000000000000000000000000 Binary files a/buddy22/src/cache.o and /dev/null differ diff --git a/buddy22/src/cppext.o b/buddy22/src/cppext.o deleted file mode 100644 index e0650499ed2ae119904e45e000e785873443ec71..0000000000000000000000000000000000000000 Binary files a/buddy22/src/cppext.o and /dev/null differ diff --git a/buddy22/src/fdd.o b/buddy22/src/fdd.o deleted file mode 100644 index 11a54be7eb322c49360c8b29a47a3568fc59c19f..0000000000000000000000000000000000000000 Binary files a/buddy22/src/fdd.o and /dev/null differ diff --git a/buddy22/src/imatrix.o b/buddy22/src/imatrix.o deleted file mode 100644 index 6fbbe53dd7f6a1a8b173efa63f0fd4b33b6eade4..0000000000000000000000000000000000000000 Binary files a/buddy22/src/imatrix.o and /dev/null differ diff --git a/buddy22/src/kernel.o b/buddy22/src/kernel.o deleted file mode 100644 index 14615dcd7c6d5e002dfe48f88273f68bc3d89372..0000000000000000000000000000000000000000 Binary files a/buddy22/src/kernel.o and /dev/null differ diff --git a/buddy22/src/libbdd.a b/buddy22/src/libbdd.a deleted file mode 100644 index 00484d799de93ccf3621c2b3c09d71264c955ff2..0000000000000000000000000000000000000000 Binary files a/buddy22/src/libbdd.a and /dev/null differ diff --git a/buddy22/src/pairs.o b/buddy22/src/pairs.o deleted file mode 100644 index 371f8c41570b1cc6aade895a1cff99182110c1b3..0000000000000000000000000000000000000000 Binary files a/buddy22/src/pairs.o and /dev/null differ diff --git a/buddy22/src/prime.o b/buddy22/src/prime.o deleted file mode 100644 index ee37b83bfaf0fccd2de2e400f5327bc8636c25a3..0000000000000000000000000000000000000000 Binary files a/buddy22/src/prime.o and /dev/null differ diff --git a/buddy22/src/reorder.o b/buddy22/src/reorder.o deleted file mode 100644 index 9eac038ea51d38d21bf4297cd6aeac7624f24669..0000000000000000000000000000000000000000 Binary files a/buddy22/src/reorder.o and /dev/null differ diff --git a/buddy22/src/tree.o b/buddy22/src/tree.o deleted file mode 100644 index 14fda4bd9e8ee0f08a8690b832131006fda7c803..0000000000000000000000000000000000000000 Binary files a/buddy22/src/tree.o and /dev/null differ