Experiments and Artifacts for "Action-Based Model Checking: Logic, Automata, and Reduction" by Stephen F. Siegel and Yihao Yan, CAV 2020 The VM was created using VirtualBox and the Lubuntu linux distribution. It is assigned 14GB RAM, which is enough for all but one of the experiments (see below). For our runs, we used a 256 GB linux machine. For details on how the software was installed and configured, see vm_notes.txt. The user name and password are both "user". The following command line tools are in the PATH: rpa: our RERS property analyzer raa: our RERS automaton analyzer mcrers: our model checker for RERS problems spin: the well-known model checker Spin The source code for rpa, raa, and mcrers can be found in the directory mcrers. Specific experimental claims are made in Section 6 of the paper. These can be replicated as described below. ---------------------------------------------------------------------------- Experiment #1: property analyzer Claim in paper: "...each edition of RERS includes a number of problems, each of which comes with 20 LTL formulas. The numbers of problems for years 2016--2019 are, in order, 20, 15, 3, and 9, for a total 47 problems, or 47*20=940 distinct model checking tasks. We used the McRERS property analyzer to analyze these formulas to determine which are interruptible...The results show that all formulas from 2016 and 2019 are interruptible.... In 2017, 22 of the 300 formulas are not interruptible; these include GF¬a111_SIGTRAP G[a71_SIGVTALRM → X¬a71_SIGVTALRM] G[(a59_SIGUSR1 ∧ X[(¬a112_SIGHUP)Ua59_SIGUSR1]) → FGa104_SIGPIPE] In 2018, 3 of the 60 formulas are not interruptible. The total runtime for the analysis of all 940 formulas was 18 seconds." Replication: The RERS problems can be found in directory mcrers/data. The 2016 problems are in subdirectory 2016, etc. This directory contains subdirectories for each problem: problem101, problem102, etc. Within each problem directory is a RERS dot file specifying the parallel composition of labeled transition systems (e.g., problem101.dot) and a text file specifying the LTL properties to be checked (e.g., problem101-properties.txt). The property file contains a sequence of properties such as this: #1: true ( ((c0_t8 => (!c0_t7 U c0_t3)) W (c0_t4 | c0_t2)) ) where #1 is the ID number of the property, true is the expected result, and the LTL formula follows on the next line. The properties must be numbered starting from 1 (this is the RERS format). The command line tool rpa takes a list of filenames for its arguments. Each file should be a RERS property file, as described above. The tool analyzes each LTL formula and reports those that are not interruptible. It also prints a summary of the number of non-interruptible properties for each file, and a grand summary at the end for all files. To replicate this experiment, change into mcrers/data and type: make rpa The output is written to files 2016/rpa2016.txt, 2017/rpa2017.txt, etc, and is self-explanatory. The output from our previous runs are in files named rpa2016_result.txt, etc. To see the specific formulas mentioned in the paper, in rpa2017.txt search for these lines: 12. G(F(!(a111_SIGTRAP))) (true) 20. G((a71_SIGVTALRM)->(X(!(a71_SIGVTALRM)))) (false) 3. G(((a59_SIGUSR1)&(X((!(a112_SIGHUP))U(a59_SIGUSR1))))->(F(G(a104_SIGPIPE)))) (true) To remove all generated files type "make clean". ---------------------------------------------------------------------------- Experiment #2: automaton analyzer "We next used the McRERS automaton analyzer to create BAs from each of the interruptible formulas, and then to determine which of these Spot-generated BAs was not in interrupt normal form. ... Interestingly, all of the Spot-generated BAs in 2016 and 2019 were already in normal form. Four of the BAs from interruptible formulas in 2017 were not in normal form; all of these formulas had the form F[a ∨ ((¬b)Wc)]. In 2018, 6 interruptible formulas have non-normal BAs; these formulas have several different non-isomorphic forms, some of which are quite complex. The details can be seen on the online archive. The total runtime for this analysis (including writing all BAs to a file) was 32 seconds." Replication: This experiment uses the command line tool raa, which also takes a list of property files for arguments. It takes each LTL formula, determines whether the formula is interruptible, and, for those that are interruptible, it generates, and prints, a Buchi automaton. It analyzes the BA to determine whether it is in normal form, and reports any that are not in normal form. A summary is printed at the end. To replicate this experiment, from mcrers/data, type: make raa The output is written to files 2016/raa2016.txt, etc. The output from our previous runs are in files raa2016_result.txt, etc. To find the 4 non-normal BAs in 2017, search raa2017.txt for the string "Non-normal". Ditto for 2018. Also look at the summary at the end for the total numbers of non-normal BAs. ---------------------------------------------------------------------------- Experiment #3: mcrers model checker "We applied the model checker to all problems in the 2019 benchmarks. Interestingly, all 180 tasks completed, with the correct results, on a laptop with 8 GB RAM; the times are given in Figure 2. The maximum memory consumed by any task is almost exactly 8 GB. We also ran these problems with POR turned off, to measure the impact of that optimization. As is often the case with POR schemes, the difference is dramatic. The non-POR tests ran out of memory on a machine with 256 GB RAM after problem 106. We show the resources consumed for a representative task in Figure 3; this property holds, so a complete search is required. In terms of number of states or time, the performance differs by about $5$ orders of magnitude." Replication: This experiment uses the model checker, the command line tool mcrers. Typing just "mcrers" at the command line will give you the usage information. To replicate this experiment, change to directory mcrers/data/2019 and type "make mc". The output is written to files problem101/out.txt, problem102/out.txt, etc. The output from our previous runs are in files named result.txt in each problem directory. Note: All the model checking runs for 2019 can complete on a MacBook Air with 8GB RAM if no other applications are running. It uses almost the entire memory of the machine. On the VM, it might take slightly more memory. The final lines of each output file summarize the total number of problems for which the correct result was obtained---this should be all of them in every case. It also reports the total time. Example: Results: 20 right, 0 wrong, 0 unknown (time: 1.00s) The number of components can be obtained by subtracting one from the reported number of processes, e.g.: Number of processes (including property).. 9 indicates there were 8 components (the 9th is the property automaton). This gives the data reported in Fig. 2. For the data reported in the top row of Fig. 3, change to directory mcrers/data/2019/problem106 and type: time mcrers -prop 1 problem106.dot problem106-properties.txt You should see a real time under 0.1s reported at the end. Look for lines like the following for the remaining stats: Number of states saved ................... 15451 Number of transitions in state space ..... 15493 MC peak memory allocated ............... 126125168 To get the data in the bottom row, we used the 256 GB machine. You may be able to run it on systems with less memory; if virtual memory is used the time could be longer. Execute time mcrers -noPOR -prop 1 problem106.dot problem106-properties.txt This is going to take a while. When it finishes, look for lines like: Number of states saved ................... 1894166619 Number of transitions in state space ..... 13502591514 MC peak memory allocated ............... 261733012534 Time (s): 7865.00s The output from both of these runs on our 256 GB machine can be found in files prop1por.txt and prop1nopor.txt. Since the point of this last experiment (i.e., Fig. 3) is just to show that using POR saves you a lot of time and memory over not using POR, you can reach the same conclusion by choosing just about any RERS task, including smaller ones, say, a property from problem105. ---------------------------------------------------------------------------- Experiment #4: Spin comparison "We ran the latest version of Spin on these using -DCOLLAPSE compression. We show the result for just the first task in Figure 4. There is at least a 4 order of magnitude performance difference (measured in states or time) between the tools." Replication: You'll get fastest performance if you use a machine with at least 12 GB RAM. We can run it on an 8GB RAM MacBook Air, but then virtual memory is used and it is a bit slower than reported. Change to directory mcrers/data/2019/problem101. Type "make spin" to run the Spin experiment on property 1. The output indicates the number of states saved, transitions executed, memory, and time. The output from our run (on the 256 GB machine) can be found in file prop1_spin.txt. Look for lines like: 81601930 states, stored 2.0175228e+08 transitions (= stored+matched) 10945.518 total actual memory usage 287.56user 4.66system 4:52.41elapsed 99%CPU (0avgtext+0avgdata 11210916maxresident) Type "make mcrers1" to run the McRERS experiment on property 1. The output indicates the states, transitions, and memory, and (real) time is reported at the end. The output from our run can be found in file prop1_mcrers.txt. Search for lines in the output like this: Number of states saved ................... 180 Number of transitions in state space ..... 193 MC peak memory allocated ............... 50595642 0.02user 0.00system 0:00.02elapsed 96%CPU (0avgtext+0avgdata 16552maxresident) Note that McRERS memory stats are in bytes, while for Spin they are reported in MB.