Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Extracting Buchi Automata from PINS #212

Open
JakeGinesin opened this issue Aug 17, 2023 · 3 comments
Open

Extracting Buchi Automata from PINS #212

JakeGinesin opened this issue Aug 17, 2023 · 3 comments

Comments

@JakeGinesin
Copy link

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
Copy link
Contributor

jacopol commented Aug 17, 2023 •
edited
Loading

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
Copy link
Author

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
Copy link
Collaborator

alaarman commented Aug 26, 2023 via email

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@alaarman @jacopol @JakeGinesin