* symbol type
* @param
* place content type
*/
public final class PetriNetUnfolder extends PetriNetUnfolderBase> {
/**
* Build the finite Prefix of PetriNet net.
*
* @param order
* the order on events and configurations respectively is used to determine cut-off events.
* @param sameTransitionCutOff
* if true, an additional condition for cut-off events is used: An event and its companion must belong to
* the same transition from the net.
* @param stopIfAcceptingRunFound
* if false, the complete finite Prefix will be build.
* @throws AutomataOperationCanceledException
* if timeout exceeds
* @throws PetriNetNot1SafeException
*/
public PetriNetUnfolder(final AutomataLibraryServices services, final IPetriNetSuccessorProvider operand,
final EventOrderEnum order, final boolean sameTransitionCutOff, final boolean stopIfAcceptingRunFound)
throws AutomataOperationCanceledException, PetriNetNot1SafeException {
super(services, operand, order, sameTransitionCutOff, stopIfAcceptingRunFound);
}
public enum EventOrderEnum {
DBO("Depth-based Order"), ERV("Esparza Römer Vogler"), KMM("Ken McMillan"),;
private String mDescription;
EventOrderEnum(final String name) {
mDescription = name;
}
public String getDescription() {
return mDescription;
}
}
@Override
protected boolean checkInitialPlaces() {
return mUnfolding.getDummyRoot().getSuccessorConditions().stream()
.anyMatch(c -> mOperand.isAccepting(c.getPlace()));
}
@Override
protected PetriNetRun constructInitialRun() throws PetriNetNot1SafeException {
return new PetriNetRun<>(
new ConditionMarking<>(mUnfolding.getDummyRoot().getSuccessorConditions()).getMarking());
}
@Override
protected boolean addAndCheck(final Event event) throws PetriNetNot1SafeException {
return mUnfolding.addEvent(event);
}
@Override
protected PetriNetRun constructRun(final Event event) {
/**
* constructs a run over the unfolding which leads to the marking corresponding with the local configuration of
* the specified event e.
*
* uses the recursive helper-method {@code #constructRun(Event, Marking)}
*/
mLogger.debug("Marking: " + mUnfolding.getDummyRoot().getMark());
try {
return constructRun(event, mUnfolding.getDummyRoot().getConditionMark()).mRunInner;
} catch (final PetriNetNot1SafeException e) {
throw new AssertionError("Petri net not one safe for places " + e.getUnsafePlaces()
+ " but this should have been detected earlier.");
}
}
class RunAndConditionMarking {
private final PetriNetRun mRunInner;
private final ConditionMarking mMarking;
public RunAndConditionMarking(final PetriNetRun run, final ConditionMarking marking) {
mRunInner = run;
mMarking = marking;
}
}
/**
* Recursively builds a part of a run over the unfolding which leads to the marking corresponding with the local
* configuration of the specified event e.
*
* The run starts with the given Marking {@code initialMarking}
*/
private RunAndConditionMarking constructRun(final Event event, final ConditionMarking initialMarking)
throws PetriNetNot1SafeException {
assert event != mUnfolding.getDummyRoot();
assert !event.getPredecessorConditions().isEmpty();
if (EXTENDED_ASSERTION_CHECKING) {
assert !mUnfolding.pairwiseConflictOrCausalRelation(event.getPredecessorConditions());
}
PetriNetRun run = new PetriNetRun<>(initialMarking.getMarking());
ConditionMarking current = initialMarking;
for (final Condition c : event.getPredecessorConditions()) {
if (current.contains(c)) {
continue;
}
final RunAndConditionMarking result = constructRun(c.getPredecessorEvent(), current);
run = run.concatenate(result.mRunInner);
current = result.mMarking;
}
assert current != null;
final ConditionMarking finalMarking = current.fireEvent(event);
final Transition t = event.getTransition();
final PetriNetRun appendix = new PetriNetRun<>(current.getMarking(), t, finalMarking.getMarking());
run = run.concatenate(appendix);
mLogger.debug("Event : " + event);
mLogger.debug("Marking: " + run.getMarking(run.getWord().length()));
return new RunAndConditionMarking(run, finalMarking);
}
@Override
protected boolean checkRun(final IPetriNet2FiniteAutomatonStateFactory stateFactory, final PetriNetRun run)
throws AutomataOperationCanceledException, PetriNetNot1SafeException {
mLogger.info("Testing correctness of emptinessCheck");
if (!(mOperand instanceof IPetriNetTransitionProvider)) {
mLogger.warn("Will not check Unfolding because operand is constructed on-demand");
return true;
}
boolean correct;
if (run == null) {
final NestedRun automataRun = (new IsEmpty<>(mServices, (new PetriNet2FiniteAutomaton<>(mServices,
stateFactory, (IPetriNetTransitionProvider) mOperand)).getResult())).getNestedRun();
if (automataRun != null) {
// TODO Christian 2016-09-30: This assignment is useless - a bug?
correct = false;
mLogger.error("EmptinessCheck says empty, but net accepts: " + automataRun.getWord());
}
correct = automataRun == null;
} else {
final Word word = run.getWord();
if (new Accepts<>(mServices, (IPetriNetTransitionProvider) mOperand, word).getResult()) {
correct = true;
} else {
mLogger.error("Result of EmptinessCheck, but not accepted: " + word);
correct = false;
}
}
mLogger.info("Finished testing correctness of emptinessCheck");
return correct;
}
}