Package net.automatalib.modelchecker.ltsmin

Class LTSminLTLParser

java.lang.Object

net.automatalib.modelchecker.ltsmin.LTSminLTLParser

public final class LTSminLTLParser
extends Object

A parser that verifies the syntax of LTL formulae of LTSmin.

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:

• 'letter' checks that each register is named "letter". This is used by DFA-based hypotheses and MealyMachine-based hypotheses with alternating input/output labels.
• 'io' checks that each register is named "input" or "output". This is used by MealyMachine-based hypotheses with synchronous labeling.

Method Summary

Modifier and Type	Method	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).

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Method Detail

requireValidLetterFormula

public static String requireValidLetterFormula(String formula)

Checks if the given formula adheres to LTSmin's expected format ('letter' flavor).

Parameters:

formula - the formula to parse / validate

Returns:

formula

Throws:

IllegalArgumentException - if the formula does not adhere to LTSmin's expected format ('letter' flavor)

See Also:

DFA2ETFWriter, Mealy2ETFWriterAlternating

isValidLetterFormula

public static boolean isValidLetterFormula(String formula)

Checks if the given formula adheres to LTSmin's expected format ('letter' flavor).

Parameters:

formula - the formula to parse / validate

Returns:

true if the formula adheres to LTSmin's expected format ('letter' flavor), false otherwise.

See Also:

DFA2ETFWriter, Mealy2ETFWriterAlternating

requireValidIOFormula

public static String requireValidIOFormula(String formula)

Checks if the given formula adheres to LTSmin's expected format ('io' flavor).

Parameters:

formula - the formula to parse / validate

Returns:

formula

Throws:

IllegalArgumentException - if the formula does not adhere to LTSmin's expected format ('io' flavor)

See Also:

Mealy2ETFWriterIO

isValidIOFormula

public static boolean isValidIOFormula(String formula)

Checks if the given formula adheres to LTSmin's expected format ('io' flavor).

Parameters:

formula - the formula to parse / validate

Returns:

true if the formula adheres to LTSmin's expected format ('io' flavor), false otherwise.

See Also:

Mealy2ETFWriterIO