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 in traces)
• 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"])