From 00219e7e9b24ee2298a7d0d977afdf123a6de88b Mon Sep 17 00:00:00 2001 From: Julien Date: Wed, 19 Jul 2017 21:40:40 +0800 Subject: rename all READM.rst to README.md Change-Id: I95930de9fefd0897bd0b75d2aeb5a1d731332dad Signed-off-by: Julien --- .../src/tests/j-verigraph-generator/README.md | 54 ++++++++++++++++++++++ 1 file changed, 54 insertions(+) create mode 100644 verigraph/service/src/tests/j-verigraph-generator/README.md (limited to 'verigraph/service/src/tests/j-verigraph-generator/README.md') diff --git a/verigraph/service/src/tests/j-verigraph-generator/README.md b/verigraph/service/src/tests/j-verigraph-generator/README.md new file mode 100644 index 0000000..c796af7 --- /dev/null +++ b/verigraph/service/src/tests/j-verigraph-generator/README.md @@ -0,0 +1,54 @@ +.. This work is licensed under a Creative Commons Attribution 4.0 International License. +.. http://creativecommons.org/licenses/by/4.0 + +CODE\_GENERATOR Java serializer and formatter + +UTILITY Contains utility methods used by other modules + +JSON\_GENERATOR Interactive module to generate the configuration files +(default names are "chains.json" and "config.json") "chains.json" +describes all the chains of nodes belonging to a certain scenario + +TEST\_CLASS\_GENERATOR Generates one or multiple test scenarios given +the two configuration files above (default names are "chains.json" and +"config.json") All the test scenarios have to be placed in the examples +folder (i. e. under "j-verigraph/service/src/tests/examples"). Here is +the script help: + +test\_class\_generator.py -c -f -o + +Supposing the module gets executed from the project root directory (i.e. +"j-verigraph"), a sample command is the following: + +service/src/tests/j-verigraph-generator/test\_class\_generator.py -c +"service/src/tests/j-verigraph-generator/examples/budapest/chains.json" +-f +"service/src/tests/j-verigraph-generator/examples/budapest/config.json" +-o "service/src/tests/examples/Scenario" + +Keep in mind that in the previous command "Scenario" represents a prefix +which will be followed by an underscore and an incremental number +starting from 1, which represents the n-th scenario starting from the +previously mentioned "chains.json" file (this file can indeed contain +multiple chains). + +TEST\_GENERATOR Generates a file which performs the verification test +through Z3 (theorem prover from Microsoft Research) given a certain +scenario generated with the above snippet. All the test modules have to +be placed under the "tests" directory (i.e. under +"j-verigraph/service/src/tests"). Here is the module help: + +test\_generator.py -i -o -s -d + +Supposing the module gets executed from the project root directory (i.e. +"j-verigraph") a sample command given the previously generated scenario +is the following: + +service/src/tests/j-verigraph-generator/test\_generator.py -i +service/src/tests/examples/Scenario\_1.java -o +service/src/tests/Test.java -s user1 -d webserver + +The aforementioned "Test.java" file can be compiled and executed +normally. Its output will be either "SAT" or "UNSAT". For possible +statistics the test is repeated 10 times and the average execution time +in seconds is printed to the console. -- cgit 1.2.3-korg