public final class LTSminLTLParser extends Object
The syntax definition is based on the grammar in the paper LTSmin: High-Performance Language-Independent Model Checking.
This parser offers two flavors of formulae which correspond to the two types of LTSmin model-checker currently available in AutomataLib:
DFA
-based hypotheses and MealyMachine
-based hypotheses with alternating input/output labels.MealyMachine
-based hypotheses with synchronous labeling.Modifier and Type | Method and Description |
---|---|
static boolean |
isValidIOFormula(String formula)
Checks if the given formula adheres to LTSmin's expected format ('io' flavor).
|
static boolean |
isValidLetterFormula(String formula)
Checks if the given formula adheres to LTSmin's expected format ('letter' flavor).
|
static String |
requireValidIOFormula(String formula)
Checks if the given formula adheres to LTSmin's expected format ('io' flavor).
|
static String |
requireValidLetterFormula(String formula)
Checks if the given formula adheres to LTSmin's expected format ('letter' flavor).
|
public static String requireValidLetterFormula(String formula)
formula
- the formula to parse / validateformula
IllegalArgumentException
- if the formula does not adhere to LTSmin's expected format ('letter' flavor)DFA2ETFWriter
,
Mealy2ETFWriterAlternating
public static boolean isValidLetterFormula(String formula)
formula
- the formula to parse / validatetrue
if the formula adheres to LTSmin's expected format ('letter' flavor), false
otherwise.DFA2ETFWriter
,
Mealy2ETFWriterAlternating
public static String requireValidIOFormula(String formula)
formula
- the formula to parse / validateformula
IllegalArgumentException
- if the formula does not adhere to LTSmin's expected format ('io' flavor)Mealy2ETFWriterIO
public static boolean isValidIOFormula(String formula)
formula
- the formula to parse / validatetrue
if the formula adheres to LTSmin's expected format ('io' flavor), false
otherwise.Mealy2ETFWriterIO
Copyright © 2020. All rights reserved.