Uses of Package
eu.iv4xr.framework.extensions.ltl
Packages that use eu.iv4xr.framework.extensions.ltl
Package
Description
This package provides the following features:
The classes
LTL and BoundedLTL implementing Linear Temporal Logic
formulas, and the bounded variation of them.Provide a class,
GameWorldModel, that can be used as a model of a
"computer game".-
Classes in eu.iv4xr.framework.extensions.ltl used by eu.iv4xr.framework.extensions.ltlClassDescriptionRepresenting a witness execution.Representing a test suite produced by
BasicModelChecker.testSuite(List, Function, int, boolean).Bounded LTL is a variation of LTL.Internal state for tracking the formula-state.Represent a 'trace' of an execution.Represent a Buchi automaton.Representing a transition in a Buchi automaton.Should be hashable and implements equals as well!An LTL formula is evaluated on a sequence of 'states' (to be more precise, a sequence of pairs (states,transitions)).An LTL formula is evaluated on a sequence of pairs (states,transitions).Provides a representation LTL formulas and a DSL for constructing them.For representing "phi || psi".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.An abstract class representing a predicate over finite sequences, defining a minimum interface needed to evaluate such a predicate on a given sequence. -
Classes in eu.iv4xr.framework.extensions.ltl used by eu.iv4xr.framework.extensions.ltl.gameworldmodelClassDescriptionShould be hashable and implements equals as well!An LTL formula is evaluated on a sequence of 'states' (to be more precise, a sequence of pairs (states,transitions)).An LTL formula is evaluated on a sequence of pairs (states,transitions).
-
Classes in eu.iv4xr.framework.extensions.ltl used by eu.iv4xr.framework.mainConcepts