diff --git a/src/main/config/tinaConfigTime.json b/src/main/config/tinaConfigTime.json
index e5ba03ce9ec7cc8c64f1bb9c7fab6aea7081039d..93c8763a11055722990a3e8b0de9769110dc402d 100644
--- a/src/main/config/tinaConfigTime.json
+++ b/src/main/config/tinaConfigTime.json
@@ -1,5 +1,5 @@
{
- "tina" : "-S -s 1 -c 0 -t 0 -b 0 -m 0 -v -NET -stats",
+ "tina" : "-W -s 1 -c 0 -t 0 -b 0 -m 0 -v -NET -stats",
"pathto" : "",
"sift" : "",
"struct" : ""
diff --git a/src/main/java/de/tudresden/inf/st/pnml/flatter/Main.java b/src/main/java/de/tudresden/inf/st/pnml/flatter/Main.java
index 08b125757f1fbcdef7d69953bccc4f0ca6ae8a3b..0d63e3f13e2bcca567b76944ec373383fb4432fa 100644
--- a/src/main/java/de/tudresden/inf/st/pnml/flatter/Main.java
+++ b/src/main/java/de/tudresden/inf/st/pnml/flatter/Main.java
@@ -32,7 +32,8 @@ public class Main {
// parse the global not flatted petri net
// pnmlPath = "../pnml-relast-nets/src/main/resources/useCaseNets/RoboticUseCase-TopLayer.pnml";
- pnmlPath = "/home/fa/Desktop/pick_and_place.pnml"; //src/main/resources/minimaltimed.pnml
+// pnmlPath = "src/main/resources/minimaltimed.pnml";
+ pnmlPath = "/home/fa/Desktop/pick_and_place.pnml"; //src/main/resources/minimaltimed.pnml
configPath = "src/main/config/tinaConfigTime.json";
PetriNet petriNet = PnmlParser.parsePnml(pnmlPath).get(0);
diff --git a/src/main/java/de/tudresden/inf/st/pnml/flatter/tina/NdrioProxy.java b/src/main/java/de/tudresden/inf/st/pnml/flatter/tina/NdrioProxy.java
index 937a1d052a93be857d7f2c7e4244d8f00cf92432..19c92dae5967cc294f1a1d9adea50d0d28d731b9 100644
--- a/src/main/java/de/tudresden/inf/st/pnml/flatter/tina/NdrioProxy.java
+++ b/src/main/java/de/tudresden/inf/st/pnml/flatter/tina/NdrioProxy.java
@@ -192,8 +192,16 @@ public class NdrioProxy extends AbstractTinaProxy{
finalLineContent.append(" [");
finalLineContent.append(a.asInputSignalTransition().getMutualTransitionInformation().getDMin());
finalLineContent.append(",");
- finalLineContent.append(a.asInputSignalTransition().getMutualTransitionInformation().getDMax());
- finalLineContent.append("]");
+ if(a.asInputSignalTransition().getMutualTransitionInformation().getDMax() < 0)
+ {
+ finalLineContent.append("w[");
+ }
+ else
+ {
+ finalLineContent.append(a.asInputSignalTransition().getMutualTransitionInformation().getDMax());
+ finalLineContent.append("]");
+ }
+
}
}
diff --git a/src/main/java/de/tudresden/inf/st/pnml/flatter/transform/SignalFlatter.java b/src/main/java/de/tudresden/inf/st/pnml/flatter/transform/SignalFlatter.java
index 4fc260e1d65c9e7addac571d944d95190a2651c6..b2cc5359f67fa16e947acdce9aea1ad63cc787e9 100644
--- a/src/main/java/de/tudresden/inf/st/pnml/flatter/transform/SignalFlatter.java
+++ b/src/main/java/de/tudresden/inf/st/pnml/flatter/transform/SignalFlatter.java
@@ -43,7 +43,8 @@ public class SignalFlatter extends Flatter{
String targetId = TemplateConstants.INPUT_SIGNAL_PLACE_ACTIVE + "-" + entry.getKey() + "-base";
String targetId2 = TemplateConstants.INPUT_SIGNAL_PLACE_INACTIVE + "-" + entry.getKey() + "-base";
- Place coreInPlace = getPlaceByID(petriNet, targetId);
+ Place coreActivePlace = getPlaceByID(petriNet, targetId);
+ Place coreInactivePlace = getPlaceByID(petriNet, targetId2);
for (InputSignalBinding isb : entry.getValue().get(0).getStaticInputSignalBindingList()) {
if (isb.getInputSignalID().equals(entry.getKey())) {
@@ -55,45 +56,100 @@ public class SignalFlatter extends Flatter{
}
}
}
-
- int andCount = 0;
- int orCount = 0;
+
for (int i = 0; i < entry.getValue().size(); i++) {
String actToInActId = TemplateConstants.INPUT_SIGNAL_TRANSITION_TO_INACTIVE + "-" + entry.getKey() + "-base";
String inActToActId = TemplateConstants.INPUT_SIGNAL_TRANSITION_TO_ACTIVE + "-" + entry.getKey() + "-base";
+ InputSignalTransition t = entry.getValue().get(i);
+ String tIntId = TemplateConstants.TIMED_TRANISTION_TEMPLATE_TIMED_INTERRUPT_TRANSITION +"-"+ t.getId() + "-" + 0;
+ InputSignalTransition tInt = getTransitionByID(petriNet, tIntId).asInputSignalTransition();
+
boolean isActiveSignal = false;
- for (InputSignalBinding isb : entry.getValue().get(i).getStaticInputSignalBindingList()) {
+ for (InputSignalBinding isb : t.getStaticInputSignalBindingList()) {
if (isb.getInputSignalID().equals(entry.getKey())) {
isActiveSignal = isb.getInputSignalValue() == 1;
break;
}
}
- // build AND-based clauses
+
+
+ if(t.getInputSignalClause().printExp().contains("NOT " + entry.getKey()))
+ {
+ t = tInt;
+ tInt = entry.getValue().get(i);
+ }
+
+
+ // build AND-based and regular clauses
if (!entry.getValue().get(i).getInputSignalClause().printExp().contains("OR")) {
- if (andCount == 0) {
- createAndIncludeArc(topPage, "IoTransitionToSignal-" + entry.getKey() + "-base", entry.getValue().get(i), coreInPlace);
- createAndIncludeArc(topPage, "IoTransitionFromSignal-" + entry.getKey() + "-base", coreInPlace, entry.getValue().get(i));
+ // REGULAR AND
+ if (i == 0) {
+ createAndIncludeArc(topPage, "IoTransitionToSignal-" + entry.getKey() + "-base", t, coreActivePlace);
+ createAndIncludeArc(topPage, "IoTransitionFromSignal-" + entry.getKey() + "-base", coreActivePlace, t);
petriNet.flushTreeCache();
} else {
- attachANDSignalNetToBaseSignalNet(petriNet, entry.getValue().get(i),
+ attachANDSignalNetToBaseSignalNet(petriNet, t,
Objects.requireNonNull(getTransitionByID(petriNet, actToInActId)).asInputSignalTransition(),
- getTransitionByID(petriNet, inActToActId).asInputSignalTransition(), i, entry.getKey(), isActiveSignal);
+ getTransitionByID(petriNet, inActToActId).asInputSignalTransition(), i, entry.getKey(), isActiveSignal,false);
}
- andCount++;
+ //add not sig as or to interrupt
+ OutputSignalPlace orTruePlace = null;
+ OutputSignalPlace orFalsePlace = null;
+
+ // check if there ar or places
+ for (Place p : tInt.asInputSignalTransition().incomingPlaces()) {
+ if (p.getId().contains(TemplateConstants.INPUT_SIGNAL_PLACE_OR_CONNECTION_TRUE_PREFIX)) {
+ orTruePlace = p.asOutputSignalPlace();
+ orFalsePlace = orPlacePairs.get(orTruePlace.getId());
+ break;
+ }
+ }
+ // if not create
+ if (orTruePlace == null) {
+ Pair<OutputSignalPlace, OutputSignalPlace> res =
+ buildOrBaseNetElements(petriNet, topPage, signalCount, i, tInt, orPlacePairs);
+ orTruePlace = res._1;
+ orFalsePlace = res._2;
+ }
+
+ attachORSignalNetToBaseSignalNet(petriNet, getTransitionByID(petriNet, actToInActId).asInputSignalTransition(),
+ getTransitionByID(petriNet, inActToActId).asInputSignalTransition(), orFalsePlace,
+ orTruePlace, i, entry.getKey(), true, isActiveSignal);
+
+
+
+
}
// build OR-based clauses
if (entry.getValue().get(i).getInputSignalClause().printExp().contains("OR")) {
+ //add not sig as and to interrupt
+ if(tInt != null)
+ {
+ if (i == 0) {
+ createAndIncludeArc(topPage, "IoTransitionToSignal-" + entry.getKey() + "-base", tInt, coreInactivePlace);
+ createAndIncludeArc(topPage, "IoTransitionFromSignal-" + entry.getKey() + "-base", coreInactivePlace, tInt);
+ petriNet.flushTreeCache();
+ } else {
+ attachANDSignalNetToBaseSignalNet(petriNet, tInt.asInputSignalTransition(),
+ Objects.requireNonNull(getTransitionByID(petriNet, actToInActId)).asInputSignalTransition(),
+ getTransitionByID(petriNet, inActToActId).asInputSignalTransition(), i, entry.getKey(), isActiveSignal, true);
+ }
+
+ }
+
+
+ //REGULAR OR
// has already connected or signal connecting place?
OutputSignalPlace orTruePlace = null;
OutputSignalPlace orFalsePlace = null;
- for (Place p : entry.getValue().get(i).incomingPlaces()) {
+ for (Place p : t.incomingPlaces()) {
if (p.getId().contains(TemplateConstants.INPUT_SIGNAL_PLACE_OR_CONNECTION_TRUE_PREFIX)) {
orTruePlace = p.asOutputSignalPlace();
orFalsePlace = orPlacePairs.get(orTruePlace.getId());
@@ -103,24 +159,15 @@ public class SignalFlatter extends Flatter{
if (orTruePlace == null) {
Pair<OutputSignalPlace, OutputSignalPlace> res =
- buildOrBaseNetElements(petriNet, topPage, signalCount, i, entry.getValue().get(i), orPlacePairs);
+ buildOrBaseNetElements(petriNet, topPage, signalCount, i, t, orPlacePairs);
orTruePlace = res._1;
orFalsePlace = res._2;
}
- if (andCount == 0 && orCount == 0) {
- attachORSignalNetToBaseSignalNet(petriNet, getTransitionByID(petriNet, actToInActId).asInputSignalTransition(),
- getTransitionByID(petriNet, inActToActId).asInputSignalTransition(), orTruePlace,
- orFalsePlace, i, entry.getKey(), true, isActiveSignal);
- System.out.println("BASE");
+ attachORSignalNetToBaseSignalNet(petriNet, getTransitionByID(petriNet, actToInActId).asInputSignalTransition(),
+ getTransitionByID(petriNet, inActToActId).asInputSignalTransition(), orTruePlace,
+ orFalsePlace, i, entry.getKey(), true, isActiveSignal);
- } else {
- attachORSignalNetToBaseSignalNet(petriNet, getTransitionByID(petriNet, actToInActId).asInputSignalTransition(),
- getTransitionByID(petriNet, inActToActId).asInputSignalTransition(), orTruePlace,
- orFalsePlace, i, entry.getKey(), false, isActiveSignal);
- System.out.println("EXTEND");
- }
- orCount++;
}
}
@@ -211,10 +258,11 @@ public class SignalFlatter extends Flatter{
}
}
- private static void attachANDSignalNetToBaseSignalNet(PetriNet petriNet, InputSignalTransition transition, InputSignalTransition inactiveT, InputSignalTransition activeT, int count, String signalId, boolean isActive) {
+ private static void attachANDSignalNetToBaseSignalNet(PetriNet petriNet, InputSignalTransition transition, InputSignalTransition inactiveT, InputSignalTransition activeT, int count, String signalId, boolean isActive, boolean isNeg) {
Page topPage = petriNet.getPage(0);
+ // get copies of signal places
OutputSignalPlace aOsp = Objects.requireNonNull(getPlaceByID(petriNet, TemplateConstants.INPUT_SIGNAL_PLACE_ACTIVE + "-" + signalId + "-base")).asOutputSignalPlace().treeCopy();
OutputSignalPlace iOsp = Objects.requireNonNull(getPlaceByID(petriNet, TemplateConstants.INPUT_SIGNAL_PLACE_INACTIVE + "-" + signalId + "-base")).asOutputSignalPlace().treeCopy();
renameSignalPlace(count, signalId, aOsp, iOsp);
@@ -224,8 +272,18 @@ public class SignalFlatter extends Flatter{
createAndIncludeArc(topPage, "arc-and-3-" + signalId + "-" + count, iOsp, activeT);
createAndIncludeArc(topPage, "arc-and-4-" + signalId + "-" + count, activeT, aOsp);
- createAndIncludeArc(topPage, "IoTransitionToSignal-" + signalId + "-" + count, transition, aOsp);
- createAndIncludeArc(topPage, "IoTransitionFromSignal-" + signalId + "-" + count, aOsp, transition);
+ if(!isNeg)
+ {
+ createAndIncludeArc(topPage, "IoTransitionToSignal-" + signalId + "-" + count, transition, aOsp);
+ createAndIncludeArc(topPage, "IoTransitionFromSignal-" + signalId + "-" + count, aOsp, transition);
+ }
+ else
+ {
+ createAndIncludeArc(topPage, "IoTransitionToSignal-" + signalId + "-" + count, transition, iOsp);
+ createAndIncludeArc(topPage, "IoTransitionFromSignal-" + signalId + "-" + count, iOsp, transition);
+ }
+
+
topPage.addObject(aOsp);
topPage.addObject(iOsp);
diff --git a/src/main/java/de/tudresden/inf/st/pnml/flatter/transform/TimedTransitionFlatter.java b/src/main/java/de/tudresden/inf/st/pnml/flatter/transform/TimedTransitionFlatter.java
index 4448ca37bc2f343a09b0521dd775380a8c499254..bdd5c940b5bc35405c5fda9b2bea0d633b39a3b2 100644
--- a/src/main/java/de/tudresden/inf/st/pnml/flatter/transform/TimedTransitionFlatter.java
+++ b/src/main/java/de/tudresden/inf/st/pnml/flatter/transform/TimedTransitionFlatter.java
@@ -24,7 +24,7 @@ public class TimedTransitionFlatter extends Flatter {
TransitionInformation ti = t.asInputSignalTransition().getStaticTransitionInformation();
// check for time binding ..
- if (t.getNumToolspecific() > 0 && !(ti.getDMin() == 0.0f && ti.getDMax() == 0.0f))
+ if (t.getNumToolspecific() > 0)
{
System.out.println("[FLATTER] Found Timed Transition" + t.getId());
timedTransitions.add(t);
@@ -92,60 +92,88 @@ public class TimedTransitionFlatter extends Flatter {
// ### Flat Interrupt Arcs
// String interruptTemplateTransitionId = TemplateConstants.TIMED_TRANISTION_TEMPLATE_TIMED_INTERRUPT_TRANSITION +"-"+ t.getId();
// Transition interruptTemplateTransition = getTransitionByID(petriNet, interruptTemplateTransitionId);
- //tI.asInputSignalTransition().setMutualTransitionInformation(tI.asInputSignalTransition().getStaticTransitionInformation());
+ //tI.asInputSignalTransition().setMutualTransitionInformation(tI.asInputSignalTransition().getStaticTransitionInformation())
int interrupt_count = 0;
- for (Arc ia:t_interruptIn_Arc){
- interrupt_count++;
+ // add interrupt arc for signal interrupt
+ if(t.asInputSignalTransition().getStaticInputSignalBindingList().getNumChild() > 0)
+ {
PetriNet intTransTemplate = SignalTemplates.getInterruptTransitionTemplate(t.getId() + "-" + interrupt_count);
includeTemplateInstance(petriNet, intTransTemplate, ti.getSubNet(), ti.getLocation());
String interruptTemplateTransitionId = TemplateConstants.TIMED_TRANISTION_TEMPLATE_TIMED_INTERRUPT_TRANSITION +"-"+ t.getId() + "-" + interrupt_count;
Transition interruptTemplateTransition = getTransitionByID(petriNet, interruptTemplateTransitionId);
- ia.setTarget(interruptTemplateTransition);
createAndIncludeArc(topPage, pfId+ "-to-" + interruptTemplateTransitionId, p_firing,interruptTemplateTransition); //firing place to interrupt transition
createAndIncludeArc(topPage, interruptTemplateTransitionId + "-to-" + prId,interruptTemplateTransition, p_ready); //interrupt transition to ready place
- createAndIncludeArc(topPage, interruptTemplateTransitionId + "-to-" + ia.getSource().getId(),interruptTemplateTransition, ia.getSource()); //arc to return interrupting token
for(Arc oa:t_interruptOut_Arc)
{
- if(interrupt_count == 1)
+ if(interrupt_count == 0)
oa.setSource(interruptTemplateTransition);
else
createAndIncludeArc(topPage, interruptTemplateTransitionId+ "-to-" + oa.getTarget().getId(), interruptTemplateTransition,oa.getTarget()); // add interrupt out arcs
}
+ interrupt_count++;
}
- petriNet.flushTreeCache();
- // ### Flat interrupt signals
- for(InputSignalBinding iisb:t_interrupting_Signals)
- {
- interrupt_count++;
+ // add regular interrupt arcs
+ for (Arc ia:t_interruptIn_Arc){
+
+
PetriNet intTransTemplate = SignalTemplates.getInterruptTransitionTemplate(t.getId() + "-" + interrupt_count);
includeTemplateInstance(petriNet, intTransTemplate, ti.getSubNet(), ti.getLocation());
String interruptTemplateTransitionId = TemplateConstants.TIMED_TRANISTION_TEMPLATE_TIMED_INTERRUPT_TRANSITION +"-"+ t.getId() + "-" + interrupt_count;
Transition interruptTemplateTransition = getTransitionByID(petriNet, interruptTemplateTransitionId);
+ ia.setTarget(interruptTemplateTransition);
+
createAndIncludeArc(topPage, pfId+ "-to-" + interruptTemplateTransitionId, p_firing,interruptTemplateTransition); //firing place to interrupt transition
createAndIncludeArc(topPage, interruptTemplateTransitionId + "-to-" + prId,interruptTemplateTransition, p_ready); //interrupt transition to ready place
+ createAndIncludeArc(topPage, interruptTemplateTransitionId + "-to-" + ia.getSource().getId(),interruptTemplateTransition, ia.getSource()); //arc to return interrupting token
+
for(Arc oa:t_interruptOut_Arc)
{
- if(interrupt_count == 1)
+ if(interrupt_count == 0)
oa.setSource(interruptTemplateTransition);
else
createAndIncludeArc(topPage, interruptTemplateTransitionId+ "-to-" + oa.getTarget().getId(), interruptTemplateTransition,oa.getTarget()); // add interrupt out arcs
- }
- // TODO: move isb
- interruptTemplateTransition.asInputSignalTransition().getMutualInputSignalBindingList().add(iisb);
+ }
+ interrupt_count++;
}
petriNet.flushTreeCache();
+// // ### Flat interrupt signals
+// for(InputSignalBinding iisb:t_interrupting_Signals)
+// {
+// interrupt_count++;
+// PetriNet intTransTemplate = SignalTemplates.getInterruptTransitionTemplate(t.getId() + "-" + interrupt_count);
+// includeTemplateInstance(petriNet, intTransTemplate, ti.getSubNet(), ti.getLocation());
+//
+// String interruptTemplateTransitionId = TemplateConstants.TIMED_TRANISTION_TEMPLATE_TIMED_INTERRUPT_TRANSITION +"-"+ t.getId() + "-" + interrupt_count;
+// Transition interruptTemplateTransition = getTransitionByID(petriNet, interruptTemplateTransitionId);
+// createAndIncludeArc(topPage, pfId+ "-to-" + interruptTemplateTransitionId, p_firing,interruptTemplateTransition); //firing place to interrupt transition
+// createAndIncludeArc(topPage, interruptTemplateTransitionId + "-to-" + prId,interruptTemplateTransition, p_ready); //interrupt transition to ready place
+//
+// for(Arc oa:t_interruptOut_Arc)
+// {
+// if(interrupt_count == 1)
+// oa.setSource(interruptTemplateTransition);
+// else
+// createAndIncludeArc(topPage, interruptTemplateTransitionId+ "-to-" + oa.getTarget().getId(), interruptTemplateTransition,oa.getTarget()); // add interrupt out arcs
+// }
+//
+// // TODO: move isb
+// interruptTemplateTransition.asInputSignalTransition().getMutualInputSignalBindingList().add(iisb);
+// }
+// petriNet.flushTreeCache();
+
+
// ### Flat Error Arcs
String tEId = TemplateConstants.TIMED_TRANISTION_TEMPLATE_TIMED_ERROR_TRANSITION +"-"+ t.getId();
Transition tE = getTransitionByID(petriNet, tEId);
diff --git a/src/main/resources/minimaltimed.pnml b/src/main/resources/minimaltimed.pnml
index 3039e8ce55ef5994a65e72b2638068a998ae3556..46467e14fb9c6ea9e06c81916ebef5bb6841d3a7 100644
--- a/src/main/resources/minimaltimed.pnml
+++ b/src/main/resources/minimaltimed.pnml
@@ -23,6 +23,25 @@
</graphics>
</place>
+ <place id="p3">
+ <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1">
+ <location>none</location>
+ <subnet>none</subnet>
+ </toolspecific>
+ <initialMarking>
+ <text>1</text>
+ </initialMarking>
+ <name>
+ <text>p3</text>
+ <graphics>
+ <offset x="0" y="0" />
+ </graphics>
+ </name>
+ <graphics>
+ <position x="0" y="0"/>
+ </graphics>
+ </place>
+
<place id="p2">
<toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1">
<location>none</location>
@@ -126,7 +145,14 @@
<dmax>10</dmax>
<type>discreteTransitionType</type>
<inputsignalbindings>
+ <inputsignalbinding>
+ <transitionID>t1</transitionID>
+ <inputsignalID>s1</inputsignalID>
+ <initialvalue>1</initialvalue>
+ <isInterrupting>0</isInterrupting>
+ </inputsignalbinding>
</inputsignalbindings>
+ <inputsignalclause>NOT s1</inputsignalclause>
</toolspecific>
<name>
<text>t1</text>
@@ -142,16 +168,23 @@
<arc id="Arc1" source="p1" target="t1">
</arc>
+ <arc id="Arc11" source="p3" target="t1">
+ </arc>
+
+
<arc id="Arc2" source="t1" target="p2">
</arc>
<arc id="Arc3" source="p_interrupting" target="t1">
+ </arc>
+
+ <arc id="Arc4" source="t1" target="p1">
<toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1">
<type>interrupt</type>
</toolspecific>
</arc>
- <arc id="Arc4" source="t1" target="p_interrupted">
+ <arc id="Arc41" source="t1" target="p3">
<toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1">
<type>interrupt</type>
</toolspecific>
diff --git a/src/main/resources/templates/InputSignal.pnml b/src/main/resources/templates/InputSignal.pnml
index ca4f3a2e329c6aa0d3f25d0ad89c1508a169822b..ecdc63426f3f76705fa915e289a86ee9245c40e0 100644
--- a/src/main/resources/templates/InputSignal.pnml
+++ b/src/main/resources/templates/InputSignal.pnml
@@ -51,6 +51,8 @@
<toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1">
<location>none</location>
<subnet>none</subnet>
+ <dmin>0</dmin>
+ <dmax>-1</dmax>
<type>discreteTransitionType</type>
<inputsignalbindings>
</inputsignalbindings>
@@ -70,6 +72,8 @@
<toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1">
<location>none</location>
<subnet>none</subnet>
+ <dmin>0</dmin>
+ <dmax>-1</dmax>
<type>discreteTransitionType</type>
<inputsignalbindings>
</inputsignalbindings>