Regexes as variables

[bestchai]

Texada currently supports two options for the atomic propositions in an LTL property:

• The atomic propositions are variables which take on every possible event in the trace as a value, i.e. x and y in G(x->XFy)

• The atomic propositions are constant taking on only one value, i.e. open in G(open->XFy).

We would like to allow a third option, allowing the values to vary, but in a restricted manner, by putting in regexes as atomic propositions, for example

G("[0-9]* is EATING" -> !y)

We'd like to only mine properties with 0 is EATING, 1 is EATING, 2 is EATING, etc., as the first event.

Implementation note:

Note that is may be better to implement this option as some sort of two-argument option (is this possible) instead of just telling Texada what the regex is, as we do for constants. (For constants, the formula has to be written with the constants in the right place and the -e option has to be given with the name of the constant). So, for example

G(x->!y) --bind-to-regex x "[0-9]* is EATING"

This is because it's possible we might want to search for

G("[0-9]* is EATING" -> !y)

with y also restricted to "[0-9]* is EATING" , but to be bound independently. Simply writing

G("[0-9]* is EATING" -> !"[0-9]* is EATING")

it is not clear whether the two "variables" are distinct or not (is this a restriction of G(x->!x) or G(x->!y?).

[Issue created by carolemieux: 2015-07-29]
[Last updated on bitbucket: 2016-09-06]

[Comment created by carolemieux: 2016-09-06]
this keeps coming up in all possible applications of Texada. Build it. Possibly encompass constant events in this.

probably wanna have options like
--regex-bind var-name regex

http://stackoverflow.com/questions/8175723/vector-arguments-in-boost-program-options