Package owl.translations.ltl2ldba

Class SymmetricLDBAConstruction<B extends GeneralizedBuchiAcceptance>

java.lang.Object

owl.translations.ltl2ldba.SymmetricLDBAConstruction<B>

All Implemented Interfaces:

Function<LabelledFormula,AnnotatedLDBA<Map<Integer,EquivalenceClass>,SymmetricProductState,B,SortedSet<SymmetricEvaluatedFixpoints>,BiFunction<Integer,EquivalenceClass,Set<SymmetricProductState>>>>

public final class SymmetricLDBAConstruction<B extends GeneralizedBuchiAcceptance>
extends Object
implements Function<LabelledFormula,AnnotatedLDBA<Map<Integer,EquivalenceClass>,SymmetricProductState,B,SortedSet<SymmetricEvaluatedFixpoints>,BiFunction<Integer,EquivalenceClass,Set<SymmetricProductState>>>>

Method Summary

Modifier and Type	Method	Description
AnnotatedLDBA<Map<Integer,EquivalenceClass>,SymmetricProductState,B,SortedSet<SymmetricEvaluatedFixpoints>,BiFunction<Integer,EquivalenceClass,Set<SymmetricProductState>>>	apply(LabelledFormula input)
MutableAutomaton<Either<Map<Integer,EquivalenceClass>,SymmetricProductState>,B>	applyWithShortcuts(LabelledFormula formula)	Construct and LDBA and remove states from initial component accepting a safety languages that have a corresponding state in the accepting component.
static <B extends GeneralizedBuchiAcceptance> SymmetricLDBAConstruction<B>	of(Class<? extends B> clazz)

Methods inherited from class java.lang.Object

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

Methods inherited from interface java.util.function.Function

andThen, compose

Method Detail

of

public static <B extends GeneralizedBuchiAcceptance> SymmetricLDBAConstruction<B> of(Class<? extends B> clazz)

apply

public AnnotatedLDBA<Map<Integer,EquivalenceClass>,SymmetricProductState,B,SortedSet<SymmetricEvaluatedFixpoints>,BiFunction<Integer,EquivalenceClass,Set<SymmetricProductState>>> apply(LabelledFormula input)

Specified by:

apply in interface Function<LabelledFormula,AnnotatedLDBA<Map<Integer,EquivalenceClass>,SymmetricProductState,B extends GeneralizedBuchiAcceptance,SortedSet<SymmetricEvaluatedFixpoints>,BiFunction<Integer,EquivalenceClass,Set<SymmetricProductState>>>>

applyWithShortcuts

public MutableAutomaton<Either<Map<Integer,EquivalenceClass>,SymmetricProductState>,B> applyWithShortcuts(LabelledFormula formula)

Construct and LDBA and remove states from initial component accepting a safety languages that have a corresponding state in the accepting component.

Parameters:

formula - the LTL formula for which the LDBA is constructed.

Returns:

An LDBA with deduplicated states recognising safety languages.