verigraph/service/src/tests/j-verigraph-generator/README.md

   1 .. This work is licensed under a Creative Commons Attribution 4.0 International License.
   2 .. http://creativecommons.org/licenses/by/4.0
   3
   4 CODE\_GENERATOR Java serializer and formatter
   5
   6 UTILITY Contains utility methods used by other modules
   7
   8 JSON\_GENERATOR Interactive module to generate the configuration files
   9 (default names are "chains.json" and "config.json") "chains.json"
  10 describes all the chains of nodes belonging to a certain scenario
  11
  12 TEST\_CLASS\_GENERATOR Generates one or multiple test scenarios given
  13 the two configuration files above (default names are "chains.json" and
  14 "config.json") All the test scenarios have to be placed in the examples
  15 folder (i. e. under "j-verigraph/service/src/tests/examples"). Here is
  16 the script help:
  17
  18 test\_class\_generator.py -c -f -o
  19
  20 Supposing the module gets executed from the project root directory (i.e.
  21 "j-verigraph"), a sample command is the following:
  22
  23 service/src/tests/j-verigraph-generator/test\_class\_generator.py -c
  24 "service/src/tests/j-verigraph-generator/examples/budapest/chains.json"
  25 -f
  26 "service/src/tests/j-verigraph-generator/examples/budapest/config.json"
  27 -o "service/src/tests/examples/Scenario"
  28
  29 Keep in mind that in the previous command "Scenario" represents a prefix
  30 which will be followed by an underscore and an incremental number
  31 starting from 1, which represents the n-th scenario starting from the
  32 previously mentioned "chains.json" file (this file can indeed contain
  33 multiple chains).
  34
  35 TEST\_GENERATOR Generates a file which performs the verification test
  36 through Z3 (theorem prover from Microsoft Research) given a certain
  37 scenario generated with the above snippet. All the test modules have to
  38 be placed under the "tests" directory (i.e. under
  39 "j-verigraph/service/src/tests"). Here is the module help:
  40
  41 test\_generator.py -i -o -s -d
  42
  43 Supposing the module gets executed from the project root directory (i.e.
  44 "j-verigraph") a sample command given the previously generated scenario
  45 is the following:
  46
  47 service/src/tests/j-verigraph-generator/test\_generator.py -i
  48 service/src/tests/examples/Scenario\_1.java -o
  49 service/src/tests/Test.java -s user1 -d webserver
  50
  51 The aforementioned "Test.java" file can be compiled and executed
  52 normally. Its output will be either "SAT" or "UNSAT". For possible
  53 statistics the test is repeated 10 times and the average execution time
  54 in seconds is printed to the console.