diff --git a/NEWS b/NEWS index d476b16ac..40770e934 100644 --- a/NEWS +++ b/NEWS @@ -80,6 +80,8 @@ New in spot 2.0.3a (not yet released) * A new example page shows how to test the equivalence of two LTL/PSL formulas. https://spot.lrde.epita.fr/tut04.html + * The concepts.html page now lists all named properties + used by automata. Bug fixes: diff --git a/doc/org/concepts.org b/doc/org/concepts.org index 0d6576a01..bcf07b09d 100644 --- a/doc/org/concepts.org +++ b/doc/org/concepts.org @@ -1026,3 +1026,47 @@ These automata properties are encoded into the [[file:hoa.org::#property-bits][H be preserved when building a processing pipeline using the shell. However the HOA format has support for more properties that do not correspond to any =twa= flag. + +* Named properties for automata + :PROPERTIES: + :CUSTOM_ID: named-properties + :END: + +In addition to [[#proeprty-flags][property flags]], automata in Spot can be tied to an +arbitrary number of objects via a system of named properties that is +implemented mostly as an =std::map= between =std::string= and =void*=. + +A property can be used to store additional information about the +automaton, that is not usually available via the automaton interface. +The property can be set via the =twa::set_named_prop(key, value)= +method, and queried with the =twa::get_named_prop(key)= template +method. + +Here is a list of named properties currently used inside Spot: + +| key name | (pointed) value type | description | +|---------------------+--------------------------------+-----------------------------------------------------------------------------------------------------------------------------------| +| ~automaton-name~ | ~std::string~ | A name for the automaton, for instance to display in the HOA format. | +| ~product-states~ | ~const spot::product_states~ | A vector of pair of states giving the left and right operand of each state in a product automaton. | +| ~state-names~ | ~std::vector~ | A vector naming each state of the automaton, for display purpose. | +| ~highlight-edges~ | ~std::map~ | A map of (edge number, color number) for highlighting the output. | +| ~highlight-states~ | ~std::map~ | A map of (state number, color number) for highlighting the output. | +| ~incomplete-states~ | ~std::set~ | A set of states numbers that should be displayed as incomplete. Used internally by ~print_dot()~ when truncating large automata. | + +Objects referenced via named properties are automatically destroyed +when the automaton is destroyed, but this can be altered by passing a +custom destructor as a third parameter to =twa::set_named_prop()=. + +These properties should be considered short-lived. They are usually +not propagated to new automata that are created via transformation, +unless the algorithme has been explicitely implemented to preserve +that property. Algorithm that update the automaton in place should +probably call =release_named_properties()= to ensure they do not +inadvertently keep a stale property. + +Most of the above properties are related to the graphical display of +automata, or to their output in the [[file:hoa.org::#named-properties][HOA format]]. So they are usually +set right before the automaton is output. The notable exception is +=product-states=, which is a property present in automata returned by +=spot::product()= function in case it is necessary to know the origins +of each state. diff --git a/doc/org/hoa.org b/doc/org/hoa.org index 4fae27970..71a3c2267 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -692,15 +692,18 @@ The logic of not cluttering the output with all of =!terminal=, so only one of those is emitted unless =-Hv= is used. ** Named properties + :PROPERTIES: + :CUSTOM_ID: named-properties + :END: In addition to the bit properties discussed above, a TωA can carry named properties of any type. When attaching a property to a TωA, you only supply a name for the property, a pointer, and an optional destructor function. -They are currently two named properties related to the HOA format. +They are currently two [[file:concepts.org::#named-properties][named properties]] related to the HOA format. -- =name= :: Is a string that stores the name of the automaton (the one given after =name:= in the HOA format) +- =automaton-name= :: Is a string that stores the name of the automaton (the one given after =name:= in the HOA format) - =state-names= :: is a vector of strings that stores the name of the states (in case states are named in the HOA format) You can see these properties being preserved when an automaton is read and then immediately output: diff --git a/spot/twa/twa.hh b/spot/twa/twa.hh index 3664d1ff9..91cae55e9 100644 --- a/spot/twa/twa.hh +++ b/spot/twa/twa.hh @@ -961,6 +961,9 @@ namespace spot /// /// When the automaton is destroyed, the \a destructor function will /// be called to destroy the attached object. + /// + /// See https://spot.lrde.epita.fr/concepts.html#named-properties + /// for a list of named properties used by Spot. void set_named_prop(std::string s, void* val, std::function destructor); @@ -975,6 +978,9 @@ namespace spot /// /// The object will be automatically destroyed when the automaton /// is destroyed. + /// + /// See https://spot.lrde.epita.fr/concepts.html#named-properties + /// for a list of named properties used by Spot. template void set_named_prop(std::string s, T* val) { @@ -993,6 +999,9 @@ namespace spot /// not include the pointer. /// /// Returns a nullptr if no such named property exists. + /// + /// See https://spot.lrde.epita.fr/concepts.html#named-properties + /// for a list of named properties used by Spot. template T* get_named_prop(std::string s) const {