flie: The Formal Language Inference Engine
Options for flie can be specified in the JSON format. (Don't forget commas between every two properties!)
The properties to specify are:
literals: propositional variables that will be part of positive or negative traces (not obligatory. If omitted, will be filled by everything occurring
- positive: traces (paths) that the formula should model. They are formatted as the initial and the lasso part,
separated by a vertical bar (|). Both parts consist of timesteps separated by a semi-colon (;).
Each timestep contains the literals (propositional variables) that hold true in it, separated by a comma (,). If none of the literals
is true in a timestep, it should be either empty, or a reserved word "null".
- negative: traces that the formula should not model. the same format as the property positive
- number-of-formulas: how many formulas flie should find (default: 1)
- max-depth-of-formula: maximum depth of any formula found by flie (default: 5)
- operators: a list of LTL operators allowed in a formula (default: ["F", "->", "&", "|", "U", "G", "X"])