Companion web page

for

Modularization of Regression Verification for Reactive Systems
Alexander Weigl, Mattias Ulbrich and Daniel Lentzsch

isola20_experiments.zip

The program can be found under VerifAPS/verifaps-lib in the branch develop. The experiments are also parts of the repository: aps-rvt/examples/ppumod

The zip file contains a folder for each experiments:

• XX_YY — files for the experiments Revision XX vs. Revision YY
  • args.txt — Arguments of the command line program, containing the contracts
  • log.txt — Log file of running the program
  • Scenario*_Final.{st,xml} — Input source files. The *.st files are extracted from the XML file by using ./prepare.sh
  • output_1 — Generated output files
    • ic3.xmv — nuxmv commands
    • Frame_abstracted.st — abstracted frames
    • FrameNameOld_FrameNameNew.sm{v,t} — SMV files for comparing both frames
• prepare.sh — preprocessing for XML (PCLOpenXML) files
• time.sh — extracts timings from log files
• loc.sh — extracts LoCs from log files
• run.sh — runs experiments with normal arguments (args.txt)
• classic.sh — runs experiments without modularisation