Skip to content

Latest commit

 

History

History
80 lines (68 loc) · 5.49 KB

test-alloy2smt-results.md

File metadata and controls

80 lines (68 loc) · 5.49 KB

Results of test_alloy2smt.py

Instructions for generating these results are in test_alloy2smt.py

Total models: 74

alloy2smt translating 74 Alloy models to smt2 file:

file cannot be found: 0 java.lang.UnsupportedOperationException: 35 java.lang.RuntimeException: 1 java.lang.IndexOutOfBoundsException: 1 other error: 0 supported to translate to cvc: 37

running cvc4 on 37 supported files from above:

cvc4 file error: 4

For remaining 33 files:

  • cvc4 total queries run: 86
  • cvc4 unknown: 64
  • cvc4 sat: 11
  • cvc4 unsat: 11

Results of CVC4 per file

Running cvc4 on 1 queries in expert-models/3zltn65gds66b6f4q3lvbtgdkb6snmuu-alloy/hc-atd/converge.als Running cvc4 on 1 queries in expert-models/7d25ioxqmue65lp6ntzz735gpbg4fmgq-amazon-snapshot-spec/textbookSnapshotIsolation.als Running cvc4 on 24 queries in expert-models/7z32luflamhdcixvt6nwznnud4oi6dbr-MSV/Algorithms/LC-Lenses/lc-lenses.als Running cvc4 on 8 queries in expert-models/7z32luflamhdcixvt6nwznnud4oi6dbr-MSV/CaseStudies/ETL_SCD/etl_scd.als Running cvc4 on 5 queries in expert-models/7z32luflamhdcixvt6nwznnud4oi6dbr-MSV/CaseStudies/OLAPUsagePrefs/OLAPUsagePrefs.als Running cvc4 on 1 queries in expert-models/7z32luflamhdcixvt6nwznnud4oi6dbr-MSV/Puzzles/FarmerCrossing/farmer_pt.als Running cvc4 on 36 queries in expert-models/7z32luflamhdcixvt6nwznnud4oi6dbr-MSV/Systems/ElevatorSPL/elevator_spl_events.als PROBLEM: not finding result for all queries - discarding file Running cvc4 on 2 queries in expert-models/7z32luflamhdcixvt6nwznnud4oi6dbr-MSV/Systems/HotelLocking/HotelExact.als Running cvc4 on 2 queries in expert-models/7z32luflamhdcixvt6nwznnud4oi6dbr-MSV/Systems/HotelLocking/HotelVar.als Running cvc4 on 2 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/algorithms/discovery/INSLabel.als Running cvc4 on 1 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/algorithms/distributed-hashtable/chord2.als Running cvc4 on 6 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/algorithms/distributed-hashtable/chordbugmodel.als Running cvc4 on 3 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/algorithms/gc/marksweepgc.als PROBLEM: not finding result for all queries - discarding file Running cvc4 on 1 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/algorithms/mapping/view-backing.als Running cvc4 on 1 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/algorithms/multicasting/iolus.als Running cvc4 on 3 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/algorithms/mutex/dijkstra-2-process.als Running cvc4 on 1 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/algorithms/synchronsation/sync.als Running cvc4 on 2 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/logic/syllogism/syllogism.als Running cvc4 on 2 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/models/file-system/file_system.als Running cvc4 on 7 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/models/firewire/firewire.als PROBLEM: not finding result for all queries - discarding file Running cvc4 on 1 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/models/java/javatypes.als Running cvc4 on 2 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/models/java/javatypes_soundness.als Running cvc4 on 2 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/models/logic/philosophers.als Running cvc4 on 5 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/models/microsoft-com/com.als PROBLEM: not finding result for all queries - discarding file Running cvc4 on 2 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/models/transport/railway.als Running cvc4 on 2 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/paper-examples/jackson-cacm-2019/origin-tracking.als Running cvc4 on 1 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/puzzles/coloring/color-australia.als Running cvc4 on 2 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/puzzles/farmer-chicken-fox/farmer.als Running cvc4 on 2 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/puzzles/tower-hanoi/hanoi.als Running cvc4 on 1 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/simple-models/books/birthday.als Running cvc4 on 1 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/simple-models/genealogy/genealogy.als Running cvc4 on 1 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/simple-models/no-solution/trivial.als Running cvc4 on 1 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/simple-models/state-machine/flip-flop.als Running cvc4 on 1 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/simple-models/state-machine/reset-flipflop-with-enable.als Running cvc4 on 1 queries in expert-models/gumxtrzzbkrtwi7jtwyu7eibi3fwhgmf-models/utilities/time/overlapping-ranges.als Running cvc4 on 1 queries in expert-models/lkicptlz3eklrbu7ppmltlkebwrvzhdq-zigbee-alloy-svn-to-git/trunk/base/random_event.als Running cvc4 on 2 queries in expert-models/oujlbmnutprdhddstyudppn7t35n43os-CANBus/CANBus.als

Notes

  • the smt2 input files all contain (assert true) (check-sat) (get-model)
  • when cvc4 returns "unknown" for check-sat, according to: cvc5/cvc5#3427 "When CVC4 says "unknown", by the SMT-LIB standard, it is required to response to get-model queries" -- "with the "best" guess so far" thus all these cvc4 runs return a model, but there it is not known to be a satisfying model