Dear Spot devs,
I am not sure how I am supposed to work with Kripke structures (which I
imported using ltsmin) or `twa_product` (which I obtained using
`otf_product` on the Kripke structure).
In the screenshot below I can invoke 'exclusive_word' with no problems on a
`kripke` and `twa_product` but the same is not true for 'contains' which
returns a type error.
The way I found to invoke 'contains' without errors is to use 'save' and
then 'automaton' to read that same file again in order to get `twa_graph`
as expected by `contains`. I am not sure this workaround is what the devs
had in mind.
Thank you for clarifying,
PierreG
[image: image.png]
Dear Spot devs,
Is there a way for Spot to perform the alphabet abstraction available in
GOAL as triggered with the `-a` switch when invoking the `alphabet` command?
I paste the GOAL documentation about it below.
Thank you,
Pierre.
- Alphabet -NAMEalphabet - Manipulate the alphabet of an automaton or a
game.SYNOPSISalphabet -s [ -ap ] FILE_OR_LVALalphabet -e EXPR [ -ap ]
FILE_OR_LVALalphabet -c EXPR [ -ap ] FILE_OR_LVALalphabet -r EXPR [ -ap ]
FILE_OR_LVALalphabet -a EXPR [-R | -A | -S EXPR | -P EXPR | -ap ]
FILE_OR_LVALDESCRIPTIONManipulate the alphabet of an automaton (or a game).
This operation is directly applied to the input automaton. The returned
value is always the new alphabet of the automaton (or the new atomic
propositions if -ap is present).
-s Simply return the alphabet of the input automaton or game.
-ap Return the atomic propositions (or classical symbols) instead of the
alphabet.
-e Expand the alphabet by a list of propositions.
-c Contract the alphabet by removing a list of propositions.
-r Rename the propositions based on a map from a proposition to its new
name.
-a Abstract the alphabet based on a map from a predicate to its definition.
-R Retain the transition symbols in alphabet abstraction.
-A Only annotate the transitions with properties specified by -S and -P.
-S Specify the name of the property that will store the symbols on the
transitions in alphabet abstraction.
-P Specify the name of the property that will store the evaluations of the
predicates in alphabet abstraction. EXAMPLE
alphabet -e "r" aut.gff
alphabet -c "p" aut.gff
alphabet -r "p=>r,q=>s" aut.gff
alphabet -a "r=>p/\q" aut.gff
alphabet -a "r=>p/\q" -A -P "Predicates" aut.gff
