Implement an improved translation to SMV directly in Pardinus

[grayswandyr]

Currently, the translation to SMV backends is performed by an OCaml program. Furthermore, this program doesn't handle models featuring integers.

This issue is here to track a re-implementation in Pardinus/Java, also handling ints. Technically it's a Pardinus issue but we also need to keep track of it for the Alloy Analyzer.

[grayswandyr]

Reminder:

sig S{ var r : S}

check {
always (#S = 4)
} for 3 Int, exactly 4 S

yields no counterexample because the (current_ translation of # into count does not take the bound on Int into account.

[grayswandyr]

Recall Skolemizing too: this won't compile with Electrod

sig S { var r : set S}
run { some s : set S | some s } for 3 Int

fails.
Electrod:

electrod (C) 2016-2020 ONERA 1.0.0-1-geb0b02e
[E002] 00000.elo:23.13-23.20: syntax error this##S
       (some s: set this##S { 
Aborting (1.973ms).