Wrong results for `--dual` (and other curiosities)

[phheim]

Sorry, but I guess I found more bugs. The --dual option is broken in 9c52294. Consider the following realizable benchmark.

state int x
input int i

game Safety from l1 {
    loc l1 1
    loc l0 0

    from l1 to l1 with [x' <= 0] && ( ([x >= 0] && ([x' = i - 1] || [x' = -i])) || [ x + 1 = x' ])

    from l1 to l0 with true
    from l0 to l0 with true
}

When running this benchmark with podman run --rm -i sweap-9c52294:latest --synthesise --synthesis_backend=strix --dual --issy < bug_A.issy returns unrealizable which is wrong.

Without --dual I could not get an result in over an hour. Astonishingly, the equivalent benchmark with [ x + 1 = x' ] swapped with [ x' = x + 1 ], i.e.

state int x
input int i

game Safety from l1 {
    loc l1 1
    loc l0 0

    from l1 to l1 with [x' <= 0] && ( ([x >= 0] && ([x' = i - 1] || [x' = -i])) || [ x' = x + 1 ])

    from l1 to l0 with true
    from l0 to l0 with true
}

will take a very long time with --dual but without it return realizable very quickly.

To summarize, the picture looks as follows:

	Version [ x + 1 = x' ]	Version [ x' = x + 1 ]
With --dual	Unreal (WRONG)	long time
Without --dual	long time	Real (correct)

Then I also tried having both [ x' = x + 1] and [ x = x' + 1 ], i.e.

state int x
input int i

game Safety from l1 {
    loc l1 1
    loc l0 0

    from l1 to l1 with [x' <= 0] && ( ([x >= 0] && ([x' = i - 1] || [x' = -i])) || ([x + 1 = x'] && [x' = x + 1]))

    from l1 to l0 with true
    from l0 to l0 with true
}

In this case in sometimes (not always) got the following non-deterministic (!!) error. Maybe this is just my setup/container but I did not get that in other cases. So maybe this is related, maybe not.

file /tmp/tmpz58jnwc3.smv: line 43: at token "P1sNONXP_issy_part_0": syntax error
aborting 'source /tmp/tmpxxxxgc8w.txt'

Use "quit" to leave NuSMV.

Use "quit" to leave NuSMV.

Use "quit" to leave NuSMV.

Use "quit" to leave NuSMV.

Use "quit" to leave NuSMV.
Peak memory used so far: 143444
checking for compatibility with program
Traceback (most recent call last):
  File "/sweap/./src/main.py", line 335, in <module>
    main()
  File "/sweap/./src/main.py", line 253, in main
    _main(args)
  File "/sweap/./src/main.py", line 315, in _main
    mm: WrappedHOA = synthesize(program, ltl, args.tlsf, bound)
                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/sweap/src/synthesis/synthesis.py", line 86, in synthesize
    wrapped_hoa: WrappedHOA = abstract_synthesis_loop(
                              ^^^^^^^^^^^^^^^^^^^^^^^^
  File "/sweap/src/synthesis/synthesis.py", line 310, in abstract_synthesis_loop
    compatible, result = refinement_standard(
                         ^^^^^^^^^^^^^^^^^^^^
  File "/sweap/src/analysis/refinement/refinement.py", line 31, in refinement_standard
    determination, result = compatibility_checking(
                            ^^^^^^^^^^^^^^^^^^^^^^^
  File "/sweap/src/analysis/compatibility_checking/compatibility_checking.py", line 79, in compatibility_checking
    ) = there_is_mismatch_between_program_and_strategy(
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/sweap/src/analysis/compatibility_checking/compatibility_checking.py", line 474, in there_is_mismatch_between_program_and_strategy
    there_is_no_mismatch, out = model_checker.invar_check(
    ^^^^^^^^^^^^^^^^^^^^^^^^^
TypeError: cannot unpack non-iterable NotImplementedType object