alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

org: update description of support for HOA properties

Browse source 
* doc/org/hoa.org: Here.  Also mention --trust-hoa.
This commit is contained in:
Alexandre Duret-Lutz 2015-11-05 17:16:54 +01:00
parent 19cd2cda6f
commit 30037b9905
1 changed files with 24 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

46
doc/org/hoa.org
View file

@ -513,34 +513,36 @@ and likewise for =Inf(4)&Inf(5)=.
** Property bits ** Property bits
The =HOA= format supports a number of optional =property:= tokens. The =HOA= format supports a number of optional =property:= tokens.
Currently most of those are ignored by Spot, or used only to These properties can be useful to speedup certain algorithms: for
double-check automata that are read. For instance is it interesting instance it is easier to complement a deterministic automaton that is
for Spot to know that an automaton is deterministic, but this can be known to be inherently weak.
automatically determined when the automaton is read, so it is not
necessary to say so on the =property:= line. (If =property:
deterministic= is present, the parser will just make sure that the
automaton is indeed deterministic, and output an error otherwise.)
Some of the properties are not as easy to check, and will be stored
in the future.
Internally, each TωA object carries a set of named bits representing Spot stores this properties that matters to its algorithms as
properties about the automaton. Currently these properties are quite additional bits attached to each automaton. Currently the HOA parser
limited: they will tell for instance if an automaton is deterministic, ignores all the properties that are unused by Spot.
if it uses state-based acceptance (as discussed above), if it is
stutter-invariant or stutter-sensitive, if it is unambiguous, or if it Some of the supported properties are double-checked when the automaton
is inherently weak. This set of supported properties will grow in the is parsed; this is for instance the case of =deterministic=,
future. =state-based=. The parser will in fact infer these properties from the
body of the file, and then return and error if what has been declared
does not correspond to the reality.
Some supported properties (like =inherently-weak=, =unambiguous=, or
=stutter-invariant=) are not double-checked, because that would
require too much additional operations. Command-line tools that read
HOA files all take a =--trust-hoa=no= option to ignore properties that
are not double-checked by the parser.
It should be noted that these bits are only implications. When such a It should be noted that these bits are only implications. When such a
bit is false, it only means that it is unknown whether the property is bit is false, it only means that it is unknown whether the property is
true. For instance if in some algorithm you want to know whether an true. For instance if in some algorithm you want to know whether an
automaton is deterministic (the equivalent of calling =autfilt -q automaton is deterministic (the equivalent of calling =autfilt -q
--is-deterministic aut.hoa= from the command-line), you not call the --is-deterministic aut.hoa= from the command-line), you should not
method =aut->prop_deterministic()= because that only check the property call the method =aut->prop_deterministic()= because that only checks
bit, and it might be false even if the =aut= is deterministic. the property bit, and it might be false even if the =aut= is
Instead, call the function =is_deterministic(aut)=. This function deterministic. Instead, call the function =is_deterministic(aut)=.
will first test the property bit, and do the actual check if it has This function will first test the property bit, and do the actual
to. check if it has to.
Algorithms that update a TωA should call the method =prop_keep()= and Algorithms that update a TωA should call the method =prop_keep()= and
use the argument to specify which of the properties they preserve. use the argument to specify which of the properties they preserve.