search

utwente-fmt / ltsmin

The LTSmin model checking toolset
http://ltsmin.utwente.nl
BSD 3-Clause "New" or "Revised" License
51 stars 30 forks source link

Extracting Buchi Automata from PINS #212

Open JakeGinesin opened 1 year ago

JakeGinesin commented 1 year ago

With Spin, it's possible to (kind of) extract the generated Buchi automata from Promela by generating the pan file with Spin, then running ./pan -d. However, you can't directly run the language intersection emptiness check between the LTL property and the output from ./pan -d without significant pre-processing because channels, datatypes, etc aren't simplified.

I'm wondering if it's possible to extract a Promela model's Buchi Automata from the PINS interface using prom2lts. I understand prom2lts has a dependency matrix and label output options, but I don't think that'll help me in this case.

I'm also looking into using spot.

I'd be extremely thankful for any suggestions or pointers. Thanks!

jacopol commented 1 year ago

Hi, the Büchi automaton is printed in the comments with the -v flag, does that help? dve2lts-mc --ltl='[]false' elevator.3.dve --buchi-type=spotba -v Since LTSmin uses Spot for LTL to Büchi, you might also use Spot directly if you only want the BA.

JakeGinesin commented 1 year ago

Thanks for your response!

For whatever reason, I can't seem to replicate the command you suggested. Here's what I'm getting:

$ dve2lts-mc --ltl='[]false' elevator.3.dve --buchi-type=spotba -v                                                  
dve2lts-mc: LTL semantics: none
dve2lts-mc: Buchi type: spotba
dve2lts-mc: Precompiled divine module initialized
divine: error while loading shared libraries: libncurses.so.5: cannot open shared object file: No such file or directory
dve2lts-mc( 0/ 8), ** error **: File not found: /tmp/ltsmin-7nljcc/elevator.3.dve2C

Although for promela files, I am able to get it to work - however, there doesn't seem to be any sort of automaton printed in the comments:

$ prom2lts-mc --ltl='[]false' zune.pml --buchi-type=spotba -v 
prom2lts-mc: LTL semantics: none
prom2lts-mc: Buchi type: spotba
prom2lts-mc: Precompiled SpinS module initialized
SpinS Promela Compiler - version 1.1 (3-Feb-2015)
(C) University of Twente, Formal Methods and Tools group

Parsing zune.pml...
Parsing zune.pml done (0.1 sec)

Optimizing graphs...
   StateMerging changed 3 states/transitions.
   RemoveUselessActions changed 10 states/transitions.
   RemoveUselessGotos changed 1 states/transitions.
   RenumberAll changed 8 states/transitions.
   StateMerging reduces 0 states
   RemoveUselessActions reduces 3 states
   RemoveUselessGotos reduces 3 states
   RenumberAll reduces 2 states
Optimization done (0.0 sec)

Generating next-state function ...
   Instantiating processes
   Statically binding references
   Creating transitions
Generating next-state function done (0.1 sec)

Creating state vector
Creating state labels
Generating transitions/state dependency matrices (36 / 6 slots) ...
   Found        105 /        324 ( 32.4%) Guard/slot reads
   Found        113 /        216 ( 52.3%) Transition/slot tests
   Found         9,        88,        88 /       552 (  1.6%,  15.9%,  15.9%) Actions/slot r,W,w
   Found        21,        96,        96 /       216 (  9.7%,  44.4%,  44.4%) Atomics/slot r,W,w
   Found       128,        96,        96 /       216 ( 59.3%,  44.4%,  44.4%) Transition/slot r,W,w
Generating transition/state dependency matrices done (0.2 sec)

Generating guard dependency matrices (54 guards) ...
   Found        946 /      1,458 ( 64.9%) Guard/guard dependencies
   Found      1,572 /      1,944 ( 80.9%) Transition/guard writes
   Found      1,296 /      1,296 (100.0%) Transition/transition writes
   Found         48 /      1,458 (  3.3%) !MCE guards
   Found         18 /        648 (  2.8%) !MCE transitions
   Found        344 /      2,916 ( 11.8%) !ICE guards
   Found      1,750 /      1,944 ( 90.0%) !NES guards
   Found        785 /      1,296 ( 60.6%) !NES transitions
   Found      1,166 /      1,944 ( 60.0%) !NDS guards
   Found        348 /      1,944 ( 17.9%) MDS guards
   Found        222 /      1,944 ( 11.4%) MES guards
   Found        623 /      1,296 ( 48.1%) !NDS transitions
   Found         29 /        648 (  4.5%) !DNA transitions
   Found        515 /        648 ( 79.5%) Commuting actions
Generating guard dependency matrices done (1.7 sec)

Written C code to /home/synchronous/code/ltsmin/ltsmin/examples/zune.pml.spins.c
Compiled C model to zune.pml.spins
prom2lts-mc( 0/ 8), ** error **: Unable to open cgroup memory limit file /sys/fs/cgroup/memory/memory.limit_in_bytes: No such file or directory
prom2lts-mc( 0/ 8): Loading model from zune.pml
prom2lts-mc( 5/ 8): LTL layer: formula: []false
prom2lts-mc( 0/ 8): LTL layer: model already has a ``buchi_accept'' property, overriding
prom2lts-mc( 5/ 8): "[]false" is not a file, parsing as formula...
prom2lts-mc( 5/ 8): Using Spin LTL semantics
prom2lts-mc( 5/ 8): Spot LTL formula:  ! ( [] (false))
prom2lts-mc( 0/ 8): Weak Buchi automaton detected, adding non-accepting as progress label.
prom2lts-mc( 0/ 8): DFS-FIFO for weak LTL, using special progress label 55
prom2lts-mc( 0/ 8): There are 56 state labels and 2 edge labels
prom2lts-mc( 0/ 8): State length is 7, there are 37 groups
prom2lts-mc( 0/ 8): Running dfsfifo using 8 cores
prom2lts-mc( 0/ 8): Using a tree table with 2^28 elements
prom2lts-mc( 0/ 8): Successor permutation: rr
prom2lts-mc( 0/ 8): Global bits: 2, count bits: 0, local bits: 0
prom2lts-mc( 4/ 8):
prom2lts-mc( 4/ 8): Non-progress cycle FOUND at depth 91!
prom2lts-mc( 4/ 8):
prom2lts-mc( 0/ 8):
prom2lts-mc( 0/ 8): mean standard work distribution: 38.2% (states) 38.1% (transitions)
prom2lts-mc( 0/ 8):
prom2lts-mc( 0/ 8): Explored 589 states 645 transitions, fanout: 1.095
prom2lts-mc( 0/ 8): Total exploration time 0.010 sec (0.000 sec minimum, 0.009 sec on average)
prom2lts-mc( 0/ 8): States per second: 58900, Transitions per second: 64500
prom2lts-mc( 0/ 8):
prom2lts-mc( 0/ 8): Load balancer:
prom2lts-mc( 0/ 8): Splits: 0
prom2lts-mc( 0/ 8): Load transfer: 0
prom2lts-mc( 0/ 8):
prom2lts-mc( 0/ 8): Progress states detected: 0
prom2lts-mc( 0/ 8): Redundant explorations: 190.1478
prom2lts-mc( 0/ 8):
prom2lts-mc( 0/ 8): Queue width: 8B, total height: 596, memory: 0.00MB
prom2lts-mc( 0/ 8): Tree memory: 0.0MB, 18.6 B/state, compr.: 62.0%
prom2lts-mc( 0/ 8): Tree fill ratio (roots/leafs): 0.0%/0.0%
prom2lts-mc( 0/ 8): Stored 39 string chucks using 0MB
prom2lts-mc( 0/ 8): String table 'bool': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)
prom2lts-mc( 0/ 8): String table 'guard': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)
prom2lts-mc( 0/ 8): String table 'pc': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)
prom2lts-mc( 0/ 8): String table 'short': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)
prom2lts-mc( 0/ 8): String table 'int': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)
prom2lts-mc( 0/ 8): String table 'statement': 0MB pointers, 0MB tables (711.11% overhead), 36 strings (distr.: 0.50)
prom2lts-mc( 0/ 8): String table 'action': 0MB pointers, 0MB tables (8533.33% overhead), 3 strings (distr.: 0.48)
prom2lts-mc( 0/ 8): String table 'buchi': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)
prom2lts-mc( 0/ 8): String table 'LTL_bool': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)
prom2lts-mc( 0/ 8): Total memory used for chunk indexing: 0MB
prom2lts-mc( 0/ 8): Est. total memory use: 0.0MB (~2048.0MB paged-in)
prom2lts-mc( 0/ 8):
prom2lts-mc( 0/ 8): Database statistics:
prom2lts-mc( 0/ 8): Elements: 203
prom2lts-mc( 0/ 8): Nodes: 472
prom2lts-mc( 0/ 8): Misses: 0
prom2lts-mc( 0/ 8): Tests: 0
prom2lts-mc( 0/ 8): Rehashes: 0
prom2lts-mc( 0/ 8):
prom2lts-mc( 0/ 8): Memory usage statistics:
prom2lts-mc( 0/ 8): Queue: 0.0 MB
prom2lts-mc( 0/ 8): DB: 0.0 MB
prom2lts-mc( 0/ 8): Colors: 0.0 MB
prom2lts-mc( 0/ 8): Chunks: 0.0 MB
prom2lts-mc( 0/ 8): DB paged in: 2048.0 MB

But, looking into spot, I think they have what I need. They seem to have ltsmin support built in, see here.

alaarman commented 12 months ago

Hi, there seems to be some error with your installation which makes divine crash: divine: error while loading shared libraries: libncurses.so.5: cannot open shared object file: No such file or directory

To print the Buchi automaton use verbose with -v.

Best,

Alfons

From: JakeGinesin @.> Date: Friday, 25 August 2023 at 17:37 To: utwente-fmt/ltsmin @.> Cc: Subscribed @.***> Subject: Re: [utwente-fmt/ltsmin] Extracting Buchi Automata from PINS (Issue #212)

Thanks for your response!

For whatever reason, I can't seem to replicate the command you suggested. Here's what I'm getting:

$ dve2lts-mc --ltl='[]false' elevator.3.dve --buchi-type=spotba -v

dve2lts-mc: LTL semantics: none

dve2lts-mc: Buchi type: spotba

dve2lts-mc: Precompiled divine module initialized

divine: error while loading shared libraries: libncurses.so.5: cannot open shared object file: No such file or directory

dve2lts-mc( 0/ 8), error : File not found: /tmp/ltsmin-7nljcc/elevator.3.dve2C

Although for promela files, I am able to get it to work - however, there doesn't seem to be any sort of automaton printed in the comments:

$ prom2lts-mc --ltl='[]false' zune.pml --buchi-type=spotba -v

prom2lts-mc: LTL semantics: none

prom2lts-mc: Buchi type: spotba

prom2lts-mc: Precompiled SpinS module initialized

SpinS Promela Compiler - version 1.1 (3-Feb-2015)

(C) University of Twente, Formal Methods and Tools group

Parsing zune.pml...

Parsing zune.pml done (0.1 sec)

Optimizing graphs...

StateMerging changed 3 states/transitions.

RemoveUselessActions changed 10 states/transitions.

RemoveUselessGotos changed 1 states/transitions.

RenumberAll changed 8 states/transitions.

StateMerging reduces 0 states

RemoveUselessActions reduces 3 states

RemoveUselessGotos reduces 3 states

RenumberAll reduces 2 states

Optimization done (0.0 sec)

Generating next-state function ...

Instantiating processes

Statically binding references

Creating transitions

Generating next-state function done (0.1 sec)

Creating state vector

Creating state labels

Generating transitions/state dependency matrices (36 / 6 slots) ...

Found 105 / 324 ( 32.4%) Guard/slot reads

Found 113 / 216 ( 52.3%) Transition/slot tests

Found 9, 88, 88 / 552 ( 1.6%, 15.9%, 15.9%) Actions/slot r,W,w

Found 21, 96, 96 / 216 ( 9.7%, 44.4%, 44.4%) Atomics/slot r,W,w

Found 128, 96, 96 / 216 ( 59.3%, 44.4%, 44.4%) Transition/slot r,W,w

Generating transition/state dependency matrices done (0.2 sec)

Generating guard dependency matrices (54 guards) ...

Found 946 / 1,458 ( 64.9%) Guard/guard dependencies

Found 1,572 / 1,944 ( 80.9%) Transition/guard writes

Found 1,296 / 1,296 (100.0%) Transition/transition writes

Found 48 / 1,458 ( 3.3%) !MCE guards

Found 18 / 648 ( 2.8%) !MCE transitions

Found 344 / 2,916 ( 11.8%) !ICE guards

Found 1,750 / 1,944 ( 90.0%) !NES guards

Found 785 / 1,296 ( 60.6%) !NES transitions

Found 1,166 / 1,944 ( 60.0%) !NDS guards

Found 348 / 1,944 ( 17.9%) MDS guards

Found 222 / 1,944 ( 11.4%) MES guards

Found 623 / 1,296 ( 48.1%) !NDS transitions

Found 29 / 648 ( 4.5%) !DNA transitions

Found 515 / 648 ( 79.5%) Commuting actions

Generating guard dependency matrices done (1.7 sec)

Written C code to /home/synchronous/code/ltsmin/ltsmin/examples/zune.pml.spins.c

Compiled C model to zune.pml.spins

prom2lts-mc( 0/ 8), error : Unable to open cgroup memory limit file /sys/fs/cgroup/memory/memory.limit_in_bytes: No such file or directory

prom2lts-mc( 0/ 8): Loading model from zune.pml

prom2lts-mc( 5/ 8): LTL layer: formula: []false

prom2lts-mc( 0/ 8): LTL layer: model already has a ``buchi_accept'' property, overriding

prom2lts-mc( 5/ 8): "[]false" is not a file, parsing as formula...

prom2lts-mc( 5/ 8): Using Spin LTL semantics

prom2lts-mc( 5/ 8): Spot LTL formula: ! ( [] (false))

prom2lts-mc( 0/ 8): Weak Buchi automaton detected, adding non-accepting as progress label.

prom2lts-mc( 0/ 8): DFS-FIFO for weak LTL, using special progress label 55

prom2lts-mc( 0/ 8): There are 56 state labels and 2 edge labels

prom2lts-mc( 0/ 8): State length is 7, there are 37 groups

prom2lts-mc( 0/ 8): Running dfsfifo using 8 cores

prom2lts-mc( 0/ 8): Using a tree table with 2^28 elements

prom2lts-mc( 0/ 8): Successor permutation: rr

prom2lts-mc( 0/ 8): Global bits: 2, count bits: 0, local bits: 0

prom2lts-mc( 4/ 8):

prom2lts-mc( 4/ 8): Non-progress cycle FOUND at depth 91!

prom2lts-mc( 4/ 8):

prom2lts-mc( 0/ 8):

prom2lts-mc( 0/ 8): mean standard work distribution: 38.2% (states) 38.1% (transitions)

prom2lts-mc( 0/ 8):

prom2lts-mc( 0/ 8): Explored 589 states 645 transitions, fanout: 1.095

prom2lts-mc( 0/ 8): Total exploration time 0.010 sec (0.000 sec minimum, 0.009 sec on average)

prom2lts-mc( 0/ 8): States per second: 58900, Transitions per second: 64500

prom2lts-mc( 0/ 8):

prom2lts-mc( 0/ 8): Load balancer:

prom2lts-mc( 0/ 8): Splits: 0

prom2lts-mc( 0/ 8): Load transfer: 0

prom2lts-mc( 0/ 8):

prom2lts-mc( 0/ 8): Progress states detected: 0

prom2lts-mc( 0/ 8): Redundant explorations: 190.1478

prom2lts-mc( 0/ 8):

prom2lts-mc( 0/ 8): Queue width: 8B, total height: 596, memory: 0.00MB

prom2lts-mc( 0/ 8): Tree memory: 0.0MB, 18.6 B/state, compr.: 62.0%

prom2lts-mc( 0/ 8): Tree fill ratio (roots/leafs): 0.0%/0.0%

prom2lts-mc( 0/ 8): Stored 39 string chucks using 0MB

prom2lts-mc( 0/ 8): String table 'bool': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)

prom2lts-mc( 0/ 8): String table 'guard': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)

prom2lts-mc( 0/ 8): String table 'pc': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)

prom2lts-mc( 0/ 8): String table 'short': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)

prom2lts-mc( 0/ 8): String table 'int': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)

prom2lts-mc( 0/ 8): String table 'statement': 0MB pointers, 0MB tables (711.11% overhead), 36 strings (distr.: 0.50)

prom2lts-mc( 0/ 8): String table 'action': 0MB pointers, 0MB tables (8533.33% overhead), 3 strings (distr.: 0.48)

prom2lts-mc( 0/ 8): String table 'buchi': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)

prom2lts-mc( 0/ 8): String table 'LTL_bool': 0MB pointers, 0MB tables (inf% overhead), 0 strings (distr.: 0.00)

prom2lts-mc( 0/ 8): Total memory used for chunk indexing: 0MB

prom2lts-mc( 0/ 8): Est. total memory use: 0.0MB (~2048.0MB paged-in)

prom2lts-mc( 0/ 8):

prom2lts-mc( 0/ 8): Database statistics:

prom2lts-mc( 0/ 8): Elements: 203

prom2lts-mc( 0/ 8): Nodes: 472

prom2lts-mc( 0/ 8): Misses: 0

prom2lts-mc( 0/ 8): Tests: 0

prom2lts-mc( 0/ 8): Rehashes: 0

prom2lts-mc( 0/ 8):

prom2lts-mc( 0/ 8): Memory usage statistics:

prom2lts-mc( 0/ 8): Queue: 0.0 MB

prom2lts-mc( 0/ 8): DB: 0.0 MB

prom2lts-mc( 0/ 8): Colors: 0.0 MB

prom2lts-mc( 0/ 8): Chunks: 0.0 MB

prom2lts-mc( 0/ 8): DB paged in: 2048.0 MB

But, looking into spot, I think they have what I need. They seem to have ltsmin support built in, see herehttps://spot.lre.epita.fr/ipynb/ltsmin-pml.html.

— Reply to this email directly, view it on GitHubhttps://github.com/utwente-fmt/ltsmin/issues/212#issuecomment-1693554942, or unsubscribehttps://github.com/notifications/unsubscribe-auth/AAJMZ5KZ2TOOQDGE663PLPTXXDBEDANCNFSM6AAAAAA3UI23YA. You are receiving this because you are subscribed to this thread.Message ID: @.***>