Kripke.java
package edu.udel.cis.vsl.tass.kripke;
import edu.udel.cis.vsl.tass.dynamic.IF.DynamicFactoryIF;
import edu.udel.cis.vsl.tass.kripke.IF.TASSEnablerIF;
import edu.udel.cis.vsl.tass.kripke.IF.TASSStateManagerIF;
import edu.udel.cis.vsl.tass.kripke.impl.Enabler;
import edu.udel.cis.vsl.tass.kripke.impl.StateManager;
import edu.udel.cis.vsl.tass.model.IF.ModelSequence;
import edu.udel.cis.vsl.tass.predicate.IF.TASSPredicateIF;
import edu.udel.cis.vsl.tass.semantics.IF.LibraryExecutorLoaderIF;
import edu.udel.cis.vsl.tass.semantics.IF.LogIF;
import edu.udel.cis.vsl.tass.state.IF.StateFactoryIF;
import edu.udel.cis.vsl.tass.transition.IF.TransitionFactoryIF;
public class Kripke {
public static TASSStateManagerIF newStateManager(
LibraryExecutorLoaderIF loader, ModelSequence modelSequence,
DynamicFactoryIF dynamicFactory, StateFactoryIF stateFactory,
int bufferSize, LogIF log) {
return new StateManager(loader, modelSequence, dynamicFactory,
stateFactory, bufferSize, log);
}
public static TASSStateManagerIF newStateManager(
LibraryExecutorLoaderIF loader, ModelSequence modelSequence,
DynamicFactoryIF dynamicFactory, StateFactoryIF stateFactory,
int bufferSize, LogIF log, TASSPredicateIF predicate) {
return new StateManager(loader, modelSequence, dynamicFactory,
stateFactory, bufferSize, log, predicate);
}
public static TASSEnablerIF newEnabler(ModelSequence modelSequence,
DynamicFactoryIF dynamicFactory, StateFactoryIF stateFactory,
TransitionFactoryIF transitionFactory, int bufferSize, LogIF log,
boolean sequential, boolean full) {
return new Enabler(modelSequence, dynamicFactory, stateFactory,
transitionFactory, bufferSize, log, sequential, full);
}
}