diff --git a/tests/python/ipnbdoctest.py b/tests/python/ipnbdoctest.py index 4cc65d056..9331482c7 100755 --- a/tests/python/ipnbdoctest.py +++ b/tests/python/ipnbdoctest.py @@ -72,7 +72,7 @@ def sanitize(s): s = re.sub(r'Generated by graphviz version.*', 'VERSION', s) # remove Spins verbose output version - s = re.sub(r'SpinS Promela Compiler.*Compiled C model to .*pml.spins', + s = re.sub(r'SpinS Promela Compiler.*Compiled C .* to .*pml.spins', 'SpinS output', s, flags=re.DOTALL) # SVG generated by graphviz may put note at different positions diff --git a/tests/python/ltsmin-pml.ipynb b/tests/python/ltsmin-pml.ipynb index 381b6f29e..26ba73717 100644 --- a/tests/python/ltsmin-pml.ipynb +++ b/tests/python/ltsmin-pml.ipynb @@ -18,7 +18,7 @@ "version": "3.5.1" }, "name": "", - "signature": "sha256:bbe178ef6526ace33fca472e0e20c706861b6b033a70d184f5a219c60812d5b7" + "signature": "sha256:07d2378b77f0b3c281fb9907deb011c1716ab64dab3726379c60ae42d5f4dd80" }, "nbformat": 3, "nbformat_minor": 0, @@ -74,31 +74,198 @@ "output_type": "stream", "stream": "stderr", "text": [ - "SpinS Promela Compiler - version 1.0 (5-Feb-2013)\n", + "SpinS Promela Compiler - version 1.1 (3-Feb-2015)\n", "(C) University of Twente, Formal Methods and Tools group\n", "\n", - "Start parsing tmplq2ksakk.pml...done\n", + "Parsing tmpmmk02hmw.pml...\n", + "Parsing tmpmmk02hmw.pml done (0.0 sec)\n", "\n", "Optimizing graphs...\n", " StateMerging changed 0 states/transitions.\n", " RemoveUselessActions changed 2 states/transitions.\n", " RemoveUselessGotos changed 2 states/transitions.\n", " RenumberAll changed 1 states/transitions.\n", - "Optimization done\n", + "Optimization done (0.0 sec)\n", "\n", - "Generating DM information ...\n", - "Generating DM information done\n", + "Generating next-state function ...\n", + " Instantiating processes\n", + " Statically binding references\n", + " Creating transitions\n", + "Generating next-state function done (0.0 sec)\n", "\n", - "Generating guard information ...\n", - " Found 0 / 4 ( 0.0%) !MCE guards.\n", - " Found 3 / 8 ( 37.5%) !IMC guards.\n", - " Found 6 / 6 (100.0%) !NES guards.\n", - " Found 6 / 6 (100.0%) !NDS guards.\n", - " Found 6 / 6 (100.0%) !visibilities.\n", - "Generating guard information done\n", + "Creating state vector\n", + "Creating state labels\n", + "Generating transitions/state dependency matrices (2 / 3 slots) ... \n", "\n", - "Written C model to /home/adl/git/spot/tests/python/tmplq2ksakk.pml.spins.c\n", - "Compiled C model to tmplq2ksakk.pml.spins\n", + " [.......... ]\n", + " [.................... ]\n", + " [.............................. ]\n", + " [........................................ ]\n", + " [..................................................]\n", + " Found 5 / 15 ( 33.3%) Guard/slot reads \n", + "\n", + " [......................... ]\n", + " [..................................................]\n", + " Found 6 / 6 (100.0%) Transition/slot tests \n", + "\n", + " [........ ]\n", + " [................ ]\n", + " [......................... ]\n", + " [................................. ]\n", + " [......................................... ]\n", + " [..................................................]\n", + " Found 2, 4, 4 / 18 ( 11.1%, 22.2%, 22.2%) Actions/slot r,W,w \n", + "\n", + " [......................... ]\n", + " [..................................................]\n", + " Found 2, 4, 4 / 6 ( 33.3%, 66.7%, 66.7%) Atomics/slot r,W,w \n", + "\n", + " [......................... ]\n", + " [..................................................]\n", + " Found 6, 4, 4 / 6 (100.0%, 66.7%, 66.7%) Transition/slot r,W,w \n", + "Generating transition/state dependency matrices done (0.0 sec)\n", + "\n", + "Generating guard dependency matrices (5 guards) ...\n", + "\n", + " [.... ]\n", + " [........ ]\n", + " [............ ]\n", + " [................ ]\n", + " [.................... ]\n", + " [......................... ]\n", + " [............................. ]\n", + " [................................. ]\n", + " [..................................... ]\n", + " [......................................... ]\n", + " Found 3 / 12 ( 25.0%) Guard/guard dependencies \n", + "\n", + " [..... ]\n", + " [.......... ]\n", + " [............... ]\n", + " [.................... ]\n", + " [......................... ]\n", + " [.............................. ]\n", + " [................................... ]\n", + " [........................................ ]\n", + " [............................................. ]\n", + " [..................................................]\n", + " Found 8 / 10 ( 80.0%) Transition/guard writes \n", + "\n", + " Found 4 / 4 (100.0%) Transition/transition writes \n", + "\n", + " [.... ]\n", + " [........ ]\n", + " [............ ]\n", + " [................ ]\n", + " [.................... ]\n", + " [......................... ]\n", + " [............................. ]\n", + " [................................. ]\n", + " [..................................... ]\n", + " [......................................... ]\n", + " Found 2 / 12 ( 16.7%) !MCE guards \n", + "\n", + " [......................... ]\n", + " Found 1 / 2 ( 50.0%) !MCE transitions \n", + "\n", + " [.. ]\n", + " [.... ]\n", + " [...... ]\n", + " [........ ]\n", + " [.......... ]\n", + " [............ ]\n", + " [.............. ]\n", + " [................ ]\n", + " [.................. ]\n", + " [.................... ]\n", + " [...................... ]\n", + " [........................ ]\n", + " [.......................... ]\n", + " [............................ ]\n", + " [.............................. ]\n", + " [................................ ]\n", + " [.................................. ]\n", + " [.................................... ]\n", + " [...................................... ]\n", + " [........................................ ]\n", + " [.......................................... ]\n", + " [............................................ ]\n", + " [.............................................. ]\n", + " [................................................ ]\n", + " [..................................................]\n", + " Found 7 / 25 ( 28.0%) !ICE guards \n", + "\n", + " [..... ]\n", + " [.......... ]\n", + " [............... ]\n", + " [.................... ]\n", + " [......................... ]\n", + " [.............................. ]\n", + " [................................... ]\n", + " [........................................ ]\n", + " [............................................. ]\n", + " [..................................................]\n", + " Found 10 / 10 (100.0%) !NES guards \n", + "\n", + " [............ ]\n", + " [......................... ]\n", + " [..................................... ]\n", + " [..................................................]\n", + " Found 4 / 4 (100.0%) !NES transitions \n", + "\n", + " [..... ]\n", + " [.......... ]\n", + " [............... ]\n", + " [.................... ]\n", + " [......................... ]\n", + " [.............................. ]\n", + " [................................... ]\n", + " [........................................ ]\n", + " [............................................. ]\n", + " [..................................................]\n", + " Found 8 / 10 ( 80.0%) !NDS guards \n", + "\n", + " [..... ]\n", + " [.......... ]\n", + " [............... ]\n", + " [.................... ]\n", + " [......................... ]\n", + " [.............................. ]\n", + " [................................... ]\n", + " [........................................ ]\n", + " [............................................. ]\n", + " [..................................................]\n", + " Found 0 / 10 ( 0.0%) MDS guards \n", + "\n", + " [..... ]\n", + " [.......... ]\n", + " [............... ]\n", + " [.................... ]\n", + " [......................... ]\n", + " [.............................. ]\n", + " [................................... ]\n", + " [........................................ ]\n", + " [............................................. ]\n", + " [..................................................]\n", + " Found 4 / 10 ( 40.0%) MES guards \n", + "\n", + " [............ ]\n", + " [......................... ]\n", + " [..................................... ]\n", + " [..................................................]\n", + " Found 0 / 4 ( 0.0%) !NDS transitions \n", + "\n", + " [......................... ]\n", + " Found 0 / 2 ( 0.0%) !DNA transitions \n", + "\n", + " [......................... ]\n", + " [..................................................]\n", + " [..................................................]\n", + " Found 2 / 2 (100.0%) Commuting actions \n", + "Generating guard dependency matrices done (0.0 sec)\n", + "\n", + "Written C code to /home/adl/git/spot/tests/python/tmpmmk02hmw.pml.spins.c\n", + "Compiled C code to PINS library tmpmmk02hmw.pml.spins\n", "\n" ] } @@ -127,9 +294,7 @@ "prompt_number": 3, "text": [ "ltsmin model with the following variables:\n", - " _nr_pr: int\n", " P_0._pc: pc\n", - " P_0._pid: pid\n", " P_0.a: int\n", " P_0.b: int" ] @@ -164,232 +329,232 @@ "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "0\n", - "\n", - "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=0, P_0.b=0\n", - ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "\n", + "P_0._pc=0, P_0.a=0, P_0.b=0\n", + ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", "\n", "\n", "I->0\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "1\n", - "\n", - "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=1, P_0.b=0\n", - ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "\n", + "P_0._pc=0, P_0.a=1, P_0.b=0\n", + ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", "\n", "\n", "0->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "2\n", - "\n", - "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=0, P_0.b=1\n", - ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "\n", + "P_0._pc=0, P_0.a=0, P_0.b=1\n", + ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", "\n", "\n", "0->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "3\n", - "\n", - "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=2, P_0.b=0\n", - "!"P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "\n", + "P_0._pc=0, P_0.a=2, P_0.b=0\n", + "!"P_0.a < 2" & !"P_0.b > 1" & !dead\n", "\n", "\n", "1->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "4\n", - "\n", - "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=1, P_0.b=1\n", - ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "\n", + "P_0._pc=0, P_0.a=1, P_0.b=1\n", + ""P_0.a < 2" & !"P_0.b > 1" & !dead\n", "\n", "\n", "1->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "2->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "5\n", - "\n", - "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=0, P_0.b=2\n", - ""P_0.a < 2" & "P_0.b > 1" & !dead\n", + "\n", + "P_0._pc=0, P_0.a=0, P_0.b=2\n", + ""P_0.a < 2" & "P_0.b > 1" & !dead\n", "\n", "\n", "2->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6\n", - "\n", - "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=3, P_0.b=0\n", - "!"P_0.a < 2" & !"P_0.b > 1" & dead\n", + "\n", + "P_0._pc=0, P_0.a=3, P_0.b=0\n", + "!"P_0.a < 2" & !"P_0.b > 1" & dead\n", "\n", "\n", "3->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "7\n", - "\n", - "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=2, P_0.b=1\n", - "!"P_0.a < 2" & !"P_0.b > 1" & !dead\n", + "\n", + "P_0._pc=0, P_0.a=2, P_0.b=1\n", + "!"P_0.a < 2" & !"P_0.b > 1" & !dead\n", "\n", "\n", "3->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "4->7\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "8\n", - "\n", - "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=1, P_0.b=2\n", - ""P_0.a < 2" & "P_0.b > 1" & !dead\n", + "\n", + "P_0._pc=0, P_0.a=1, P_0.b=2\n", + ""P_0.a < 2" & "P_0.b > 1" & !dead\n", "\n", "\n", "4->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "5->8\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "9\n", - "\n", - "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=0, P_0.b=3\n", - ""P_0.a < 2" & "P_0.b > 1" & dead\n", + "\n", + "P_0._pc=0, P_0.a=0, P_0.b=3\n", + ""P_0.a < 2" & "P_0.b > 1" & dead\n", "\n", "\n", "5->9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "6->6\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "10\n", - "\n", - "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=3, P_0.b=1\n", - "!"P_0.a < 2" & !"P_0.b > 1" & dead\n", + "\n", + "P_0._pc=0, P_0.a=3, P_0.b=1\n", + "!"P_0.a < 2" & !"P_0.b > 1" & dead\n", "\n", "\n", "7->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "11\n", - "\n", - "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=2, P_0.b=2\n", - "!"P_0.a < 2" & "P_0.b > 1" & !dead\n", + "\n", + "P_0._pc=0, P_0.a=2, P_0.b=2\n", + "!"P_0.a < 2" & "P_0.b > 1" & !dead\n", "\n", "\n", "7->11\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "8->11\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "12\n", - "\n", - "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=1, P_0.b=3\n", - ""P_0.a < 2" & "P_0.b > 1" & dead\n", + "\n", + "P_0._pc=0, P_0.a=1, P_0.b=3\n", + ""P_0.a < 2" & "P_0.b > 1" & dead\n", "\n", "\n", "8->12\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "9->9\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "10->10\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "13\n", - "\n", - "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=3, P_0.b=2\n", - "!"P_0.a < 2" & "P_0.b > 1" & dead\n", + "\n", + "P_0._pc=0, P_0.a=3, P_0.b=2\n", + "!"P_0.a < 2" & "P_0.b > 1" & dead\n", "\n", "\n", "11->13\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "14\n", - "\n", - "_nr_pr=1, P_0._pc=0, P_0._pid=0, P_0.a=2, P_0.b=3\n", - "!"P_0.a < 2" & "P_0.b > 1" & dead\n", + "\n", + "P_0._pc=0, P_0.a=2, P_0.b=3\n", + "!"P_0.a < 2" & "P_0.b > 1" & dead\n", "\n", "\n", "11->14\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "12->12\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "13->13\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "14->14\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text": [ - " *' at 0x7f87ac090240> >" + " *' at 0x7fe0808e0240> >" ] } ], @@ -478,9 +643,7 @@ "prompt_number": 8, "text": [ "ltsmin model with the following variables:\n", - " _nr_pr: int\n", " P_0._pc: pc\n", - " P_0._pid: pid\n", " P_0.a: int\n", " P_0.b: int" ]