Transpile Python to nuXmv source code
nuXmv 2.0.0 (but should work with any version
>= 2.0.0) and
To install it,
pip install pynuxmv
From a shell, launch:
pynuXmv <python_fname> <nuxmv_out_fname>
This will transpile
python_fname and save the result into
tests/ folder for examples.
A simple one:
from pynuxmv.main import * a = 0 b = 0 while (a + b < 2): if b == 0 and a == 1: b = 1 else: if b == 1 and a == 1: b = 0 if a == 1: a = 0 else: a = 1 ltlspec("F (a = 1 & b = 1)") ltlspec("(a = 0 & b = 0) -> F (a = 1 & b = 0)") ltlspec("(a = 1 & b = 0) -> F (a = 0 & b = 1)") ltlspec("(a = 0 & b = 1) -> F (a = 1 & b = 1)")
is converted into:
MODULE main VAR a: integer; b: integer; line: integer; ASSIGN init(a) := 0; init(b) := 0; init(line) := 1; next(line) := case line = 8 & b = 1 & a = 1: line + 1; -- if(True) line = 8: 11; -- if(False) line = 5 & b = 0 & a = 1: line + 1; -- if(True) line = 6: 12; -- end if(True) line = 5: 8; -- else line = 12 & a = 1: line + 1; -- if(True) line = 13: 17; -- end if(True) line = 12: 15; -- else line = 4 & a + b < 2: line + 1; -- while(True) line = 4: 18; -- while(False) line = 17: 4; -- loop while line = 21: 21; TRUE: line + 1; esac; next(a) := case line = 13: 0; line = 15: 1; TRUE: a; esac; next(b) := case line = 6: 1; line = 9: 0; TRUE: b; esac; LTLSPEC F (a = 1 & b = 1); LTLSPEC (a = 0 & b = 0) -> F (a = 1 & b = 0); LTLSPEC (a = 1 & b = 0) -> F (a = 0 & b = 1); LTLSPEC (a = 0 & b = 1) -> F (a = 1 & b = 1);
This nuXmv file can be run with:
nuXmv -source cmd_ltl <filename>
cmd_ltl (or, for invariant checking, the equivalent
cmd_invar) can be found in this repository.
Up to now, this simple script has many limitations:
- Limited support for
forconstruct (only with numeric
- No support for python types other than
listsupport is still very experimental)
- No support for higher structures (i.e. function calls, classes...)
- No support for concurrent execution and/or
I hope to be able to work on some of these issues in the (near) future.
Also, take a look at the
TODO.md file for other thing that can (not) be done up to now.
The following assumes that you are examining a portion of "self-contained" code (ie. code that doesn't reference variables and/or functions defined outside of such portion) that is within the limitations listed before.
Let's look at an example:
... (other code) ... start_nuxmv() b: bool = False x = 0 while (x < 10 and not b): x += 1 ltlspec("F x = 10") invarspec("!b") end_nuxmv() ... (other code) ...
Let's notice some things:
The block of code that we want to isolate and test is enclosed within two functions,
end_nuxmv(). These functions do nothing, they are just placeholders. There can be as many of these functions as you like, but they should not be nested.
bis a boolean; this information needs to be specified in order to distinguish it from an
integer, the default type assumed by
At the end of the block you specify the conditions you want your program to comply with. These can be of two kinds,
ltlspec) or invariants (
invarspec). More informations on LTL can be found on wikipedia.
Finally: how do you test this portion of code? You simply run
pynuXmvwith the name of the source
.pyfile to analyze and with the file name of the resulting
nuXmvsource code. You then launch
nuXmvon these latter file, with an appropriate commands file (such as
unify, which you can find in this repository).
Let's look at another example:
from pynuxmv.main import * x = 0 y = 1 l: list = [1,2,3] while (y < 10): x += 1 y += 1 l = l + x postcondition("y = 10", False) postcondition("x = 9", False) postcondition("l = 48", True)
list, and must be annotated as such. Here is a simple example of basically everything that you can do with lists so far (not much!)
postcondition(s: str, strong: bool)function specifies a condition that needs to be satisfied after the last line of code. The function is accompained by the
nuXmvis not always capable of establishing whether a formula is true or false; if this is the case, enabling the
strongflag will build a "stronger" condition in which previous postconditions are taken as premises; this may or may not help
nuXmvin its judgments. In this example, the three postconditions will generate the following formulae:
INVARSPEC line = 7 -> y = 10; INVARSPEC line = 7 -> x = 9; INVARSPEC ((line = 7 -> y = 10) & (line = 7 -> x = 9) ) -> (line = 7 -> l = 48);
Of course, bear in mind that if one of the premises is false the strong postcondition will be trivially true!
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.