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 Issues

Try a more problem-aware branching strategy

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

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

Use GitHub Workflows to publish jars

Investigate the new soundness bug

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)

Integrate with OSTRICH+

TEST DOES THIS SHOW UP!?

Soundness bug

A recent commit introduced a soundness bug.

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

Benchmark a version without the backwards-reachability test

Rename the Verma backend

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

This should greatly simplify the code.

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)

Rename the princess backend

Verma implementation reports unsat for at least one satisfiable instance

Soundness bug: early materialisation of products produces incorrect results

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.

Verma backend crashes for almost all inputs

Randomise instance execution order

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.

Timeouts are now crashes for at least Verma

Find-image crashes when asking Princess for the image

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

Parsing "constraint false" does not work

This may or may not include other atoms.

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

Prune products using forward and backward reachability

Enable dumping dot files

Implement the Parikh-over-and approximation

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

Investigate more eager materialisation

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.

Test the Verma backend

Verma: backlog of automata to materialise is a priority queue

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.

Path-based QE for finding images

Implement getting register assignments for nuxmv in the case of SAT

Fix the output from get-image for the Princess backend

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

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

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

amandasystems / catra Goto Github PK

catra's Issues

Recommend Projects

Recommend Topics

Recommend Org