predecessorPlaces = transitions.iterator().next().getPredecessors();
return transitions.stream().allMatch(x -> predecessorPlaces.equals(x.getPredecessors()));
}
/**
* Checks equivalent of two Petri nets. Two Petri nets are equivalent iff they accept the same language.
*
* This is a naive implementation and may be very slow.
*
* @param net1
* Petri net
* @param net2
* Petri net
* @return net1 and net2 accept the same language
* @throws AutomataLibraryException
* The operation was canceled
*/
public static & INwaInclusionStateFactory>
boolean isEquivalent(final AutomataLibraryServices services, final CRSF stateFactory,
final IPetriNetTransitionProvider net1,
final IPetriNetTransitionProvider net2) throws AutomataLibraryException {
return new IsEquivalent<>(services, stateFactory, netToNwa(services, stateFactory, net1),
netToNwa(services, stateFactory, net2)).getResult();
}
private static >
INwaOutgoingLetterAndTransitionProvider netToNwa(final AutomataLibraryServices mServices,
final CRSF stateFactory, final IPetriNetTransitionProvider net)
throws PetriNetNot1SafeException, AutomataOperationCanceledException {
return new PetriNet2FiniteAutomaton<>(mServices, stateFactory, net).getResult();
}
/**
* List hash codes of Petri net's internal objects. Useful for detecting nondeterminism. Should only be used for
* debugging.
*/
public static String printHashCodesOfInternalDataStructures(final IPetriNet net) {
final StringBuilder sb = new StringBuilder();
sb.append("HashCodes of PetriNet data structures ");
sb.append(System.lineSeparator());
int placeCounter = 0;
for (final PLACE place : net.getInitialPlaces()) {
sb.append("Place " + placeCounter + ": " + place.hashCode());
sb.append(System.lineSeparator());
placeCounter++;
}
int transitionCounter = 0;
for (final Transition trans : net.getTransitions()) {
sb.append(trans.hashCode());
sb.append("Place " + transitionCounter + ": " + trans.hashCode());
sb.append(System.lineSeparator());
transitionCounter++;
}
return sb.toString();
}
/**
* Uses finite automata to check if the result of our Petri net difference operations is correct.
*/
public static & INwaInclusionStateFactory>
boolean doDifferenceLanguageCheck(final AutomataLibraryServices services, final CRSF stateFactory,
final IPetriNetTransitionProvider minuend,
final INestedWordAutomaton subtrahend,
final IPetriNetTransitionProvider result)
throws PetriNetNot1SafeException, AutomataOperationCanceledException, AutomataLibraryException {
final AutomatonWithImplicitSelfloops subtrahendWithSelfloopsInAcceptingStates =
new AutomatonWithImplicitSelfloops<>(services, subtrahend, subtrahend.getAlphabet(),
subtrahend::isFinal);
final INestedWordAutomaton op1AsNwa =
new PetriNet2FiniteAutomaton<>(services, stateFactory, minuend).getResult();
final INwaOutgoingLetterAndTransitionProvider rcResult =
new DifferenceDD<>(services, stateFactory, op1AsNwa, subtrahendWithSelfloopsInAcceptingStates)
.getResult();
final INwaOutgoingLetterAndTransitionProvider resultAsNwa =
new PetriNet2FiniteAutomaton<>(services, stateFactory, result).getResult();
final IsIncluded isSubset = new IsIncluded<>(services, stateFactory, resultAsNwa, rcResult);
if (!isSubset.getResult()) {
final NestedWord ctx = isSubset.getCounterexample().getWord();
final ILogger logger = services.getLoggingService().getLogger(PetriNetUtils.class);
logger.error("Accepted by resulting net but not in difference of languages : " + ctx);
}
final IsIncluded isSuperset = new IsIncluded<>(services, stateFactory, rcResult, resultAsNwa);
if (!isSuperset.getResult()) {
final NestedWord ctx = isSuperset.getCounterexample().getWord();
final ILogger logger = services.getLoggingService().getLogger(PetriNetUtils.class);
logger.error("In difference of languages but not accepted by resulting net : " + ctx);
}
return isSubset.getResult() && isSuperset.getResult();
}
public static String generateStatesAndPlacesDisjointErrorMessage(final PLACE state) {
return "Currently, we require that states of the automaton are disjoint from places of Petri net. Please rename: "
+ state;
}
public static Map mergePlaces(final Set places, final UnionFind uf) {
final Map result = new HashMap<>();
for (final PLACE p : places) {
final PLACE pRep = uf.find(p);
if (pRep == null) {
result.put(p, p);
} else {
result.put(p, pRep);
}
}
return result;
}
public static Map, Transition>
mergePlaces(final IPetriNet net, final Map map) {
final Map, Transition> result = new HashMap<>();
for (final Transition oldT : net.getTransitions()) {
final ImmutableSet predecessors =
oldT.getPredecessors().stream().map(map::get).collect(ImmutableSet.collector());
final ImmutableSet successors =
oldT.getSuccessors().stream().map(map::get).collect(ImmutableSet.collector());
final Transition newT = new Transition<>(oldT.getSymbol(), predecessors, successors, 0);
result.put(oldT, newT);
}
return result;
}
public static IPetriNet mergePlaces(final AutomataLibraryServices services,
final IPetriNet net, final Map map) {
final Map, Transition> transitionMap = mergePlaces(net, map);
final BoundedPetriNet result = new BoundedPetriNet<>(services, net.getAlphabet(), false);
final Map> newPlaces = new HashMap<>();
for (final PLACE p : net.getPlaces()) {
final boolean isInitial = net.getInitialPlaces().contains(p);
final boolean isAccepting = net.isAccepting(p);
final PLACE newPlace = map.get(p);
final Pair iniAcc = newPlaces.get(newPlace);
final boolean oldIsInitial;
final boolean oldIsAccepting;
if (iniAcc == null) {
oldIsInitial = false;
oldIsAccepting = false;
} else {
oldIsInitial = iniAcc.getFirst();
oldIsAccepting = iniAcc.getSecond();
}
newPlaces.put(newPlace, new Pair<>(oldIsInitial || isInitial, oldIsAccepting || isAccepting));
}
for (final Entry> entry : newPlaces.entrySet()) {
result.addPlace(entry.getKey(), entry.getValue().getFirst(), entry.getValue().getSecond());
}
for (final Entry, Transition> entry : transitionMap.entrySet()) {
result.addTransition(entry.getValue().getSymbol(), entry.getValue().getPredecessors(),
entry.getValue().getSuccessors());
}
return result;
}
}