HoaPrintable
public class ProductControllerSynthesis extends Automaton<ProductControllerSynthesis.State,GeneralizedRabinAcceptance2<ProductControllerSynthesis.State>>
Modifier and Type | Class | Description |
---|---|---|
class |
ProductControllerSynthesis.State |
HoaPrintable.HoaOption
Modifier and Type | Field | Description |
---|---|---|
protected java.util.Map<UnaryModalOperator,FrequencySelfProductSlave> |
secondaryAutomata |
acceptance, factories, initialStates, transitions, variables, vsFactory
Constructor | Description |
---|---|
ProductControllerSynthesis(MasterAutomaton primaryAutomaton,
java.util.Map<UnaryModalOperator,FrequencySelfProductSlave> slaves,
Factories factories) |
Modifier and Type | Method | Description |
---|---|---|
TranSet<ProductControllerSynthesis.State> |
getControllerAcceptanceF(FOperator f,
java.util.Set<UnaryModalOperator> finalStates) |
|
java.util.Map<TranSet<ProductControllerSynthesis.State>,java.lang.Integer> |
getControllerAcceptanceFrequencyG(FrequencyG g,
java.util.Set<UnaryModalOperator> finalStates) |
|
TranSet<ProductControllerSynthesis.State> |
getControllerAcceptanceG(GOperator g,
java.util.Set<UnaryModalOperator> finalStates) |
|
protected void |
setAcceptance(GeneralizedRabinAcceptance2<ProductControllerSynthesis.State> acc) |
This method is important, because currently the acceptance is computed after the product is
constructed.
|
void |
toHoa(jhoafparser.consumer.HOAConsumer ho,
java.util.EnumSet<HoaPrintable.HoaOption> options) |
|
protected void |
toHoaBodyEdge(ProductControllerSynthesis.State state,
HoaConsumerExtended hoa) |
Override this method, if you want output additional edges for
state not present in
Automaton.transitions . |
generate, getAcceptance, getInitialState, getInitialStates, getStates, getSuccessors, getVariables, setInitialState, size, toHoaBody, toString
getName, toHoa
protected final java.util.Map<UnaryModalOperator,FrequencySelfProductSlave> secondaryAutomata
public ProductControllerSynthesis(MasterAutomaton primaryAutomaton, java.util.Map<UnaryModalOperator,FrequencySelfProductSlave> slaves, Factories factories)
public TranSet<ProductControllerSynthesis.State> getControllerAcceptanceF(FOperator f, java.util.Set<UnaryModalOperator> finalStates)
public java.util.Map<TranSet<ProductControllerSynthesis.State>,java.lang.Integer> getControllerAcceptanceFrequencyG(FrequencyG g, java.util.Set<UnaryModalOperator> finalStates)
public TranSet<ProductControllerSynthesis.State> getControllerAcceptanceG(GOperator g, java.util.Set<UnaryModalOperator> finalStates)
protected void setAcceptance(GeneralizedRabinAcceptance2<ProductControllerSynthesis.State> acc)
public void toHoa(jhoafparser.consumer.HOAConsumer ho, java.util.EnumSet<HoaPrintable.HoaOption> options)
toHoa
in interface HoaPrintable
toHoa
in class Automaton<ProductControllerSynthesis.State,GeneralizedRabinAcceptance2<ProductControllerSynthesis.State>>
protected void toHoaBodyEdge(ProductControllerSynthesis.State state, HoaConsumerExtended hoa)
Automaton
state
not present in
Automaton.transitions
.toHoaBodyEdge
in class Automaton<ProductControllerSynthesis.State,GeneralizedRabinAcceptance2<ProductControllerSynthesis.State>>