Package eu.iv4xr.framework.extensions.ltl

package eu.iv4xr.framework.extensions.ltl

This package provides the following features:

1. The classes LTL and BoundedLTL implementing Linear Temporal Logic formulas, and the bounded variation of them. These formulas can be evaluated on finite sequence of 'items'.
2. A bounded and lazy model-checker for checking if a target-model M1 has an execution that satisfies a specification-model M2 (and returns a witnessing execution of this). The specification-model is expressed as a finite state machine (FSM) with either a standard acceptance criterion, or an omega (more specifically, Buchi) acceptance criterion. M1 is anything that implements the interface ITargetModel.
3. An interface ITargetModel that a target system must implement, if you want to use the model checker to check it.

TODO: translation from LTLs to specification-FSMs. Probably will only support limited translation (won't allow recursion to the left-side of until).

Interface Summary

Interface	Description
IExplorableState	Should be hashable and implements equals as well!
IState	An LTL formula is evaluated on a sequence of 'states' (to be more precise, a sequence of pairs (states,transitions)).
ITargetModel
ITransition	An LTL formula is evaluated on a sequence of pairs (states,transitions).

Class Summary

Class	Description
BasicModelChecker	Provide an explicit-state bounded and lazy model checker that can be used to check if a model contains a reachable state (within a given maximum depth) satisfying some predicate q.
BasicModelChecker.MCStatistics
BasicModelChecker.Path<State>	Representing a witness execution.
BasicModelChecker.TestSuite<CoverageItem>	Representing a test suite produced by BasicModelChecker.testSuite(List, Function, int, boolean).
BoundedLTL	Bounded LTL is a variation of LTL.
BoundedLTL.WitnessTrace	Represent a 'trace' of an execution.
Buchi	Represent a Buchi automaton.
Buchi.BuchiTransition	Representing a transition in a Buchi automaton.
BuchiModelChecker	Provide an explicit-state bounded and lazy model checker that can be used to check if a model M has an execution, of up to some maximum length, that would satisfy a certain property.
LTL<State>	Provides a representation LTL formulas and a DSL for constructing them.
LTL.And<State>
LTL.LTLVerdictInfo
LTL.Next<State>
LTL.Not<State>
LTL.Now<State>
LTL.Or<State>	For representing "phi || psi".
LTL.Until<State>
LTL.WeakUntil<State>	Weak-until is not primitive in LTL-sense, but we add it as a separate class so that we can structurally recognize that a formula is a weak-until formula.
LTL2Buchi	For translating an LTL formula to a Buchi automaton.
SequencePredicate<State>	An abstract class representing a predicate over finite sequences, defining a minimum interface needed to evaluate such a predicate on a given sequence.

Enum Summary

Enum	Description
BoundedLTL.BLTLstate	Internal state for tracking the formula-state.
SATVerdict