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

[SimpleXiaohu]

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)

[amandasystems]

I found the bug! The same counter, len1, is declared twice. This situation isn't discovered by the very rudimentary input validation, and apparently leads to an invalid nuxmv encoding. A future version will address this bug.

[amandasystems]

I have added validation to address the issue now; I feel like the best approach is to reject input where the same counter is declared more than once since it suggests a mistake.