amandasystems / catra Goto Github PK

View Code? Open in Web Editor NEW

5.0 5.0 1.0 129.81 MB

A Princess theory for computing Parikh images of automata

License: Other

Scala 92.44% Makefile 0.47% Shell 1.51% Python 5.58%

catra's People

Contributors

Stargazers

Watchers

Forkers

simplexiaohu

catra's Issues

Fix the output from get-image for the Princess backend

Parsing "constraint false" does not work

This may or may not include other atoms.

Allow separate declaration of variables for counting, and assume all counters start at zero

Catch heap full exception during product materialisation and report it as a memory-out

Soundness bug

A recent commit introduced a soundness bug.

Integrate with OSTRICH+

Implement the Parikh-over-and approximation

Refactor: allow for composite Transition types and encode counters, etc, in transitions

This should greatly simplify the code.

Benchmark a version without the backwards-reachability test

TEST DOES THIS SHOW UP!?

Try a more problem-aware branching strategy

Use GitHub Workflows to publish jars

LengthCounting fails for automata accepting only the empty string

Since there are no transitions, such automata will post no constraints and therefore allow any length values. This is obviously wrong.

Rename the princess backend

Less eager Verma implementation (check constraints at every partial product)

Investigate more eager materialisation

An invalid input where the same counter is declared more than once is accepted

Commmand is:

$ ./bin/catra solve-satisfy --backend nuxmv 1.par

The contants of 1.par are:

counter int R5, len1, idx1, len1, R11, R6, R8, R9, R10, idx1, cookie_part3, R7;
synchronised {
automaton aut_cookie_part10 {
	init s32;
	s0 -> s6 [56, 56] {};
	s1 -> s5 [49, 49] {};
	s2 -> s4 [48, 48] {};
	s3 -> s7 [49, 49] {};
	s4 -> s28 [48, 48] {};
	s5 -> s8 [51, 51] {};
	s6 -> s14 [32, 32] {};
	s7 -> s18 [50, 50] {};
	s8 -> s3 [32, 32] {};
	s10 -> s17 [32, 32] {};
	s11 -> s21 [99, 99] {};
	s12 -> s25 [120, 120] {};
	s13 -> s27 [32, 32] {};
	s14 -> s23 [68, 68] {};
	s15 -> s35 [104, 104] {};
	s16 -> s13 [44, 44] {};
	s17 -> s30 [85, 85] {};
	s18 -> s2 [58, 58] {};
	s19 -> s24 [114, 114] {};
	s20 -> s10 [48, 48] {};
	s21 -> s26 [32, 32] {};
	s22 -> s9 [67, 67] {};
	s23 -> s11 [101, 101] {};
	s24 -> s36 [101, 101] {};
	s25 -> s29 [112, 112] {};
	s26 -> s34 [50, 50] {};
	s27 -> s0 [49, 49] {};
	s28 -> s37 [58, 58] {};
	s29 -> s19 [105, 105] {};
	s30 -> s22 [84, 84] {};
	s31 -> s33 [61, 61] {};
	s32 -> s12 [101, 101] {};
	s33 -> s15 [84, 84] {};
	s34 -> s1 [48, 48] {};
	s35 -> s16 [117, 117] {};
	s36 -> s31 [115, 115] {};
	s37 -> s20 [48, 48] {};
	accepting s9;
};
};
synchronised {
automaton aut_all_8_40 {
	init s11;
	s0 -> s7 [97, 97] {};
	s1 -> s10 [104, 104] {};
	s2 -> s8 [97, 97] {};
	s3 -> s0 [101, 101] {};
	s4 -> s1 [99, 99] {};
	s5 -> s6 [61, 61] {};
	s6 -> s6 [97, 110] {};
	s7 -> s4 [114, 114] {};
	s8 -> s9 [110, 110] {};
	s9 -> s5 [103, 103] {};
	s10 -> s2 [76, 76] {};
	s11 -> s3 [115, 115] {};
	accepting s6;
};
automaton aut_all_8_41 {
	init s0;
	s0 -> s0 [0, 65535] {R9 += 1};
	accepting s0;
};
automaton aut_all_8_42 {
	init s4;
	s0 -> s9 [97, 97] {};
	s1 -> s7 [97, 97] {};
	s2 -> s12 [61, 61] {};
	s3 -> s6 [104, 104] {};
	s4 -> s8 [115, 115] {};
	s5 -> s10 [98, 98] {};
	s6 -> s1 [76, 76] {};
	s7 -> s11 [110, 110] {};
	s8 -> s0 [101, 101] {};
	s9 -> s13 [114, 114] {};
	s11 -> s2 [103, 103] {};
	s12 -> s5 [110, 110] {};
	s13 -> s3 [99, 99] {};
	accepting s10;
};
};
synchronised {
automaton aut_lang0 {
	init s0;
	s0 -> s0 [0, 65535] {R6 += 1};
	accepting s0;
};
automaton aut_lang1 {
	init s0;
	accepting s0;
};
automaton aut_lang2 {
	init s0;
	s0 -> s0 [0, 65535] {R11 += 1};
	accepting s0;
};
automaton aut_lang3 {
	init s0;
	accepting s0;
};
};
synchronised {
automaton aut_all_8_50 {
	init s0;
	s0 -> s0 [0, 65535] {R5 += 1};
	accepting s0;
};
automaton aut_all_8_51 {
	init s1;
	s1 -> s0 [59, 59] {};
	s1 -> s0 [63, 63] {};
	accepting s0;
};
automaton aut_all_8_52 {
	init s0;
	s0 -> s0 [0, 65535] {R10 += 1};
	accepting s0;
};
automaton aut_all_8_53 {
	init s1;
	s1 -> s0 [59, 59] {};
	accepting s0;
};
};
synchronised {
automaton aut_10 {
	init s0;
	s0 -> s1 [59, 59] {};
	accepting s1;
};
automaton aut_11 {
	init s1;
	s0 -> s0 [0, 65535] {};
	s1 -> s0 [0, 65535] {};
	accepting s0;
};
automaton aut_12 {
	init s1;
	s1 -> s0 [59, 59] {};
	accepting s0;
};
};
synchronised {
automaton aut_l10 {
	init s0;
	s0 -> s0 [0, 65535] {};
	accepting s0;
};
automaton aut_l11 {
	init s11;
	s0 -> s8 [99, 99] {};
	s2 -> s3 [61, 61] {};
	s3 -> s10 [108, 108] {};
	s4 -> s2 [110, 110] {};
	s5 -> s12 [111, 111] {};
	s6 -> s4 [105, 105] {};
	s7 -> s6 [97, 97] {};
	s8 -> s13 [97, 97] {};
	s9 -> s1 [59, 59] {};
	s10 -> s0 [111, 111] {};
	s11 -> s5 [100, 100] {};
	s12 -> s7 [109, 109] {};
	s13 -> s9 [108, 108] {};
	accepting s1;
};
};
constraint R11 + R10 + -1*R8 = 0 ;

The output on the terminal is"

==== 1.par error: No output from nuxmv ====
java.lang.Exception: No output from nuxmv
        at uuverifiers.catra.NUXMVInstance.<init>(NUXMVBackend.scala:255)
        at uuverifiers.catra.NUXMVBackend.solveSatisfy(NUXMVBackend.scala:23)
        at uuverifiers.catra.SolveRegisterAutomata$.runInstance(SolveRegisterAutomata.scala:93)
        at uuverifiers.catra.SolveRegisterAutomata$.$anonfun$runInstances$3(SolveRegisterAutomata.scala:109)
        at uuverifiers.catra.SolveRegisterAutomata$.$anonfun$runInstances$1(SolveRegisterAutomata.scala:53)
        at uuverifiers.catra.SolveRegisterAutomata$.$anonfun$runInstances$1$adapted(SolveRegisterAutomata.scala:98)
        at scala.collection.immutable.List.foreach(List.scala:333)
        at uuverifiers.catra.SolveRegisterAutomata$.runInstances(SolveRegisterAutomata.scala:98)
        at uuverifiers.catra.SolveRegisterAutomata$.delayedEndpoint$uuverifiers$catra$SolveRegisterAutomata$1(SolveRegisterAutomata.scala:124)
        at uuverifiers.catra.SolveRegisterAutomata$delayedInit$body.apply(SolveRegisterAutomata.scala:48)
        at scala.Function0.apply$mcV$sp(Function0.scala:39)
        at scala.Function0.apply$mcV$sp$(Function0.scala:39)
        at scala.runtime.AbstractFunction0.apply$mcV$sp(AbstractFunction0.scala:17)
        at scala.App.$anonfun$main$1(App.scala:76)
        at scala.App.$anonfun$main$1$adapted(App.scala:76)
        at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)
        at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)
        at scala.collection.AbstractIterable.foreach(Iterable.scala:926)
        at scala.App.main(App.scala:76)
        at scala.App.main$(App.scala:74)
        at uuverifiers.catra.SolveRegisterAutomata$.main(SolveRegisterAutomata.scala:48)
        at uuverifiers.catra.SolveRegisterAutomata.main(SolveRegisterAutomata.scala)

Verma backend crashes for almost all inputs

Investigate the new soundness bug

Clean up the package and file/folder structure

Currently the structure of everything is a mess. We should have a consistent package structure separating the front-end from the back-end, and a folder hierarchy to match.

Soundness bug: early materialisation of products produces incorrect results

Randomise instance execution order

Verma: backlog of automata to materialise is a priority queue

Timeouts are now crashes for at least Verma

Rename the Verma backend

Refactor: replace Automaton.neighbours with Automaton.outgoing, which returns transitions

This is a preparation for the bigger refactoring of allowing for composite transitions.

Test "product of 4-state, per-transition register automaton with loop has values" OOMs

Test the Verma backend

Some instances sometimes produce a Princess crash: Proof Certificate Missing

Example instance:

counter int R0, R1, R2, R3, R4, R5;
synchronised {  // Automata constraining uri
automaton uri_0 {
  init s0;
  s0 -> s1 [109, 109];
  s1 -> s2 [111, 111];
  s2 -> s3 [110, 110];
  s3 -> s4 [103, 103];
  s4 -> s5 [111, 111];
  s5 -> s6 [100, 100];
  s6 -> s7 [98, 98];
  s7 -> s8 [58, 58];
  s8 -> s9 [47, 47];
  s9 -> s10 [47, 47];
  s10 -> s10 [0, 65535];
  accepting s10;
};
automaton uri_1 {
  init s0;
  s0 -> s0 [0, 65535] { R1 += 1 };
  accepting s0;
};
automaton uri_2 {
  init s0;
  s0 -> s1 [0, 36] { R3 += 1 };
  s0 -> s0 [0, 65535] { R2 += 1, R3 += 1 };
  s0 -> s1 [38, 42] { R3 += 1 };
  s0 -> s2 [44, 44] { R3 += 1 };
  s0 -> s1 [45, 45] { R3 += 1 };
  s0 -> s3 [46, 46] { R3 += 1 };
  s0 -> s1 [48, 62] { R3 += 1 };
  s0 -> s1 [65, 65535] { R3 += 1 };
  s1 -> s1 [0, 36] { R3 += 1 };
  s1 -> s1 [38, 42] { R3 += 1 };
  s1 -> s2 [44, 44] { R3 += 1 };
  s1 -> s1 [45, 45] { R3 += 1 };
  s1 -> s3 [46, 46] { R3 += 1 };
  s1 -> s1 [48, 62] { R3 += 1 };
  s1 -> s1 [65, 65535] { R3 += 1 };
  s2 -> s2 [0, 36] { R3 += 1 };
  s2 -> s2 [38, 42] { R3 += 1 };
  s2 -> s2 [44, 45] { R3 += 1 };
  s2 -> s9 [46, 46] { R3 += 1 };
  s2 -> s2 [48, 62] { R3 += 1 };
  s2 -> s2 [65, 65535] { R3 += 1 };
  s3 -> s1 [0, 36] { R3 += 1 };
  s3 -> s1 [38, 42] { R3 += 1 };
  s3 -> s2 [44, 44] { R3 += 1 };
  s3 -> s1 [45, 45] { R3 += 1 };
  s3 -> s3 [46, 46] { R3 += 1 };
  s3 -> s1 [48, 62] { R3 += 1 };
  s3 -> s1 [65, 114] { R3 += 1 };
  s3 -> s4 [115, 115] { R3 += 1 };
  s3 -> s1 [116, 65535] { R3 += 1 };
  s4 -> s1 [0, 36] { R3 += 1 };
  s4 -> s1 [38, 42] { R3 += 1 };
  s4 -> s2 [44, 44] { R3 += 1 };
  s4 -> s1 [45, 45] { R3 += 1 };
  s4 -> s3 [46, 46] { R3 += 1 };
  s4 -> s1 [48, 62] { R3 += 1 };
  s4 -> s1 [65, 110] { R3 += 1 };
  s4 -> s5 [111, 111] { R3 += 1 };
  s4 -> s1 [112, 65535] { R3 += 1 };
  s5 -> s1 [0, 36] { R3 += 1 };
  s5 -> s1 [38, 42] { R3 += 1 };
  s5 -> s2 [44, 44] { R3 += 1 };
  s5 -> s1 [45, 45] { R3 += 1 };
  s5 -> s3 [46, 46] { R3 += 1 };
  s5 -> s1 [48, 62] { R3 += 1 };
  s5 -> s1 [65, 98] { R3 += 1 };
  s5 -> s6 [99, 99] { R3 += 1 };
  s5 -> s1 [100, 65535] { R3 += 1 };
  s6 -> s1 [0, 36] { R3 += 1 };
  s6 -> s1 [38, 42] { R3 += 1 };
  s6 -> s2 [44, 44] { R3 += 1 };
  s6 -> s1 [45, 45] { R3 += 1 };
  s6 -> s3 [46, 46] { R3 += 1 };
  s6 -> s1 [48, 62] { R3 += 1 };
  s6 -> s1 [65, 106] { R3 += 1 };
  s6 -> s7 [107, 107] { R3 += 1 };
  s6 -> s1 [108, 65535] { R3 += 1 };
  s7 -> s7 [0, 36] { R3 += 1 };
  s7 -> s7 [38, 42] { R3 += 1 };
  s7 -> s8 [44, 44] { R3 += 1 };
  s7 -> s7 [45, 46] { R3 += 1 };
  s7 -> s7 [48, 62] { R3 += 1 };
  s7 -> s7 [65, 65535] { R3 += 1 };
  s8 -> s8 [0, 36] { R3 += 1 };
  s8 -> s8 [0, 65535];
  s8 -> s8 [38, 42] { R3 += 1 };
  s8 -> s8 [44, 46] { R3 += 1 };
  s8 -> s8 [48, 62] { R3 += 1 };
  s8 -> s8 [65, 65535] { R3 += 1 };
  s9 -> s2 [0, 36] { R3 += 1 };
  s9 -> s2 [38, 42] { R3 += 1 };
  s9 -> s2 [44, 45] { R3 += 1 };
  s9 -> s9 [46, 46] { R3 += 1 };
  s9 -> s2 [48, 62] { R3 += 1 };
  s9 -> s2 [65, 114] { R3 += 1 };
  s9 -> s10 [115, 115] { R3 += 1 };
  s9 -> s2 [116, 65535] { R3 += 1 };
  s10 -> s2 [0, 36] { R3 += 1 };
  s10 -> s2 [38, 42] { R3 += 1 };
  s10 -> s2 [44, 45] { R3 += 1 };
  s10 -> s9 [46, 46] { R3 += 1 };
  s10 -> s2 [48, 62] { R3 += 1 };
  s10 -> s2 [65, 110] { R3 += 1 };
  s10 -> s11 [111, 111] { R3 += 1 };
  s10 -> s2 [112, 65535] { R3 += 1 };
  s11 -> s2 [0, 36] { R3 += 1 };
  s11 -> s2 [38, 42] { R3 += 1 };
  s11 -> s2 [44, 45] { R3 += 1 };
  s11 -> s9 [46, 46] { R3 += 1 };
  s11 -> s2 [48, 62] { R3 += 1 };
  s11 -> s2 [65, 98] { R3 += 1 };
  s11 -> s12 [99, 99] { R3 += 1 };
  s11 -> s2 [100, 65535] { R3 += 1 };
  s12 -> s2 [0, 36] { R3 += 1 };
  s12 -> s2 [38, 42] { R3 += 1 };
  s12 -> s2 [44, 45] { R3 += 1 };
  s12 -> s9 [46, 46] { R3 += 1 };
  s12 -> s2 [48, 62] { R3 += 1 };
  s12 -> s2 [65, 106] { R3 += 1 };
  s12 -> s8 [107, 107] { R3 += 1 };
  s12 -> s2 [108, 65535] { R3 += 1 };
  accepting s8;
};
automaton uri_3 {
  init s0;
  s0 -> s0 [0, 65535] { R4 += 1, R5 += 1 };
  s0 -> s1 [0, 65535] { R5 += 1, R0 += 1 };
  s1 -> s2 [0, 65535];
  s1 -> s1 [0, 65535] { R5 += 1, R0 += 1 };
  s2 -> s2 [0, 65535];
  accepting s0, s1, s2;
};
};
constraint R1 = R5 && R2 = 10 && R3 = R5 && R4 = 10 && R0 != 0 && 9 < R5;

Note that the issue is nondeterministic: it is sometimes triggered, sometimes not.

crash when using option `--trace`

Used command:

./bin/catra solve-satisfy --trace --backend lazy regression.par

Output:

==== regression.par error: Internal exception: scala.MatchError: RemoveFacts((Connected_1092004553(all_1_0, 0))) (of class ap.proof.theoryPlugins.Plugin$RemoveFacts) ====
ap.api.SimpleAPI$SimpleAPIForwardedException: Internal exception: scala.MatchError: RemoveFacts((Connected_1092004553(all_1_0, 0))) (of class ap.proof.theoryPlugins.Plugin$RemoveFacts)
        at ap.api.SimpleAPI.evalProverResult(SimpleAPI.scala:2133)
        at ap.api.SimpleAPI.getStatusHelp(SimpleAPI.scala:2092)
        at ap.api.SimpleAPI.getStatus(SimpleAPI.scala:2082)
        at uuverifiers.catra.PrincessBasedBackend.checkSatWithRestarts(PrincessBasedBackend.scala:69)
        at uuverifiers.catra.PrincessBasedBackend.checkSat(PrincessBasedBackend.scala:56)
        at uuverifiers.catra.PrincessBasedBackend.checkSolutions(PrincessBasedBackend.scala:80)
        at uuverifiers.catra.PrincessBasedBackend.$anonfun$solveSatisfy$1(PrincessBasedBackend.scala:101)
        at uuverifiers.catra.CommandLineOptions.withProver(CommandLineOptions.scala:63)
        at uuverifiers.catra.PrincessBasedBackend.solveSatisfy(PrincessBasedBackend.scala:98)
        at uuverifiers.catra.PrincessBasedBackend.solveSatisfy$(PrincessBasedBackend.scala:96)
        at uuverifiers.catra.LazyBackend.solveSatisfy(LazyBackend.scala:12)
        at uuverifiers.catra.SolveRegisterAutomata$.runInstance(SolveRegisterAutomata.scala:93)
        at uuverifiers.catra.SolveRegisterAutomata$.$anonfun$runInstances$3(SolveRegisterAutomata.scala:109)
        at uuverifiers.catra.SolveRegisterAutomata$.$anonfun$runInstances$1(SolveRegisterAutomata.scala:53)
        at uuverifiers.catra.SolveRegisterAutomata$.$anonfun$runInstances$1$adapted(SolveRegisterAutomata.scala:98)
        at scala.collection.immutable.List.foreach(List.scala:333)
        at uuverifiers.catra.SolveRegisterAutomata$.runInstances(SolveRegisterAutomata.scala:98)
        at uuverifiers.catra.SolveRegisterAutomata$.delayedEndpoint$uuverifiers$catra$SolveRegisterAutomata$1(SolveRegisterAutomata.scala:124)
        at uuverifiers.catra.SolveRegisterAutomata$delayedInit$body.apply(SolveRegisterAutomata.scala:48)
        at scala.Function0.apply$mcV$sp(Function0.scala:39)
        at scala.Function0.apply$mcV$sp$(Function0.scala:39)
        at scala.runtime.AbstractFunction0.apply$mcV$sp(AbstractFunction0.scala:17)
        at scala.App.$anonfun$main$1(App.scala:76)
        at scala.App.$anonfun$main$1$adapted(App.scala:76)
        at scala.collection.IterableOnceOps.foreach(IterableOnce.scala:563)
        at scala.collection.IterableOnceOps.foreach$(IterableOnce.scala:561)
        at scala.collection.AbstractIterable.foreach(Iterable.scala:926)
        at scala.App.main(App.scala:76)
        at scala.App.main$(App.scala:74)
        at uuverifiers.catra.SolveRegisterAutomata$.main(SolveRegisterAutomata.scala:48)
        at uuverifiers.catra.SolveRegisterAutomata.main(SolveRegisterAutomata.scala)
Caused by: scala.MatchError: RemoveFacts((Connected_1092004553(all_1_0, 0))) (of class ap.proof.theoryPlugins.Plugin$RemoveFacts)
        at uuverifiers.parikh_theory.TracingComputation.actionToTex(TracingComputation.scala:48)
        at uuverifiers.parikh_theory.TracingComputation.$anonfun$actionHook$3(TracingComputation.scala:94)
        at scala.collection.immutable.List.map(List.scala:246)
        at scala.collection.immutable.List.map(List.scala:79)
        at uuverifiers.parikh_theory.TracingComputation.$anonfun$actionHook$2(TracingComputation.scala:94)
        at uuverifiers.parikh_theory.TracingComputation.actionHook(TracingComputation.scala:87)
        at uuverifiers.parikh_theory.TracingComputation.actionHook$(TracingComputation.scala:74)
        at uuverifiers.catra.LazyBackend$$anon$2.actionHook(LazyBackend.scala:94)
        at uuverifiers.parikh_theory.TracingComputation.$anonfun$actionHooks$1(TracingComputation.scala:101)
        at uuverifiers.parikh_theory.TracingComputation.$anonfun$actionHooks$1$adapted(TracingComputation.scala:101)
        at uuverifiers.parikh_theory.ParikhTheory.$anonfun$runHooks$1(ParikhTheory.scala:123)
        at uuverifiers.parikh_theory.ParikhTheory.$anonfun$runHooks$1$adapted(ParikhTheory.scala:122)
        at scala.collection.immutable.List.foreach(List.scala:333)
        at uuverifiers.parikh_theory.ParikhTheory.runHooks(ParikhTheory.scala:122)
        at uuverifiers.parikh_theory.ParikhTheory.runHooks$(ParikhTheory.scala:117)
        at uuverifiers.parikh_theory.RegisterCounting.runHooks(RegisterCounting.scala:11)
        at uuverifiers.parikh_theory.MonoidMapPlugin.handleConnectedInstance(MonoidMapPlugin.scala:207)
        at uuverifiers.parikh_theory.MonoidMapPlugin.$anonfun$handleConnectedInstances$1(MonoidMapPlugin.scala:155)
        at scala.collection.StrictOptimizedIterableOps.flatMap(StrictOptimizedIterableOps.scala:118)
        at scala.collection.StrictOptimizedIterableOps.flatMap$(StrictOptimizedIterableOps.scala:105)
        at scala.collection.immutable.Vector.flatMap(Vector.scala:113)
        at uuverifiers.parikh_theory.MonoidMapPlugin.handleConnectedInstances(MonoidMapPlugin.scala:155)
        at uuverifiers.parikh_theory.MonoidMapPlugin.$anonfun$handlePredicateInstance$1(MonoidMapPlugin.scala:71)
        at ap.proof.theoryPlugins.TheoryProcedure$RichActionSeq.elseDo(Plugin.scala:189)
        at uuverifiers.parikh_theory.MonoidMapPlugin.handlePredicateInstance(MonoidMapPlugin.scala:71)
        at uuverifiers.parikh_theory.PredicateHandlingProcedure.$anonfun$handleGoal$1(PrincessHelpers.scala:63)
        at scala.collection.StrictOptimizedIterableOps.flatMap(StrictOptimizedIterableOps.scala:118)
        at scala.collection.StrictOptimizedIterableOps.flatMap$(StrictOptimizedIterableOps.scala:105)
        at scala.collection.immutable.Vector.flatMap(Vector.scala:113)
        at uuverifiers.parikh_theory.PredicateHandlingProcedure.handleGoal(PrincessHelpers.scala:63)
        at uuverifiers.parikh_theory.PredicateHandlingProcedure.handleGoal$(PrincessHelpers.scala:58)
        at uuverifiers.parikh_theory.MonoidMapPlugin.handleGoal(MonoidMapPlugin.scala:22)
        at ap.proof.theoryPlugins.PluginTask.apply(Plugin.scala:424)
        at ap.proof.goal.Goal.step(Goal.scala:421)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:486)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:549)
        at ap.proof.ModelSearchProver.ap$proof$ModelSearchProver$$findModel(ModelSearchProver.scala:495)
        at ap.proof.ModelSearchProver$IncProverImpl.checkValidityDir(ModelSearchProver.scala:1108)
        at ap.api.ProofThreadRunnable$$anonfun$1.$anonfun$applyOrElse$2(ProofThread.scala:154)
        at ap.util.Timeout$.catchTimeout(Timeout.scala:100)
        at ap.api.ProofThreadRunnable$$anonfun$1.applyOrElse(ProofThread.scala:155)
        at scala.runtime.AbstractPartialFunction.apply(AbstractPartialFunction.scala:35)
        at ap.api.ProofThreadRunnable.$anonfun$run$2(ProofThread.scala:210)
        at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
        at scala.util.DynamicVariable.withValue(DynamicVariable.scala:59)
        at ap.util.Timeout$.withChecker(Timeout.scala:56)
        at ap.api.ProofThreadRunnable.run(ProofThread.scala:200)
        at java.base/java.lang.Thread.run(Thread.java:831)

Connect the Verma back-end to the CLI front-end

Front-end: warn if automata have overlapping counters in their transitions

Find-image crashes when asking Princess for the image

Verma implementation reports unsat for at least one satisfiable instance

Prune products using forward and backward reachability

Path-based QE for finding images

Implement getting register assignments for nuxmv in the case of SAT

Enable dumping dot files

Verma back-end needs timeouts for product construction (and possibly others)

Enabling proof constructions causes Princess to crash

When using RegisterCounting and enabling setConstructProofs in Princess, Princess will crash with a term-resolution related exception very likely related to the term order.