From ecf50684cf8fb1c10c6004fc471808bb13075cec Mon Sep 17 00:00:00 2001 From: SebastianEbert <sebastian.ebert@tu-dresden.de> Date: Mon, 25 Nov 2024 16:55:38 +0100 Subject: [PATCH] added models for task 2 --- models/task-2/model-one-robot-flattened.net | 144 +++++++++++ models/task-2/model-one-robot.pnml | 141 +---------- models/task-2/model-without-sync-flatted.net | 158 ++++++++++++ models/task-2/model-without-sync.pnml | 244 +++++-------------- 4 files changed, 369 insertions(+), 318 deletions(-) create mode 100644 models/task-2/model-one-robot-flattened.net create mode 100644 models/task-2/model-without-sync-flatted.net diff --git a/models/task-2/model-one-robot-flattened.net b/models/task-2/model-one-robot-flattened.net new file mode 100644 index 0000000..659c3bc --- /dev/null +++ b/models/task-2/model-one-robot-flattened.net @@ -0,0 +1,144 @@ +net FullModel +tr {CallbackInputTransition-LeftCellTopic-0-0} {CallbackCapacityPlace-LeftCellTopic-0-0} {CallbackInputPlace-LeftCellTopic-0-0} -> {CallbackConnectorPlace-LeftCellTopic-0-0} +tr {CallbackInputTransition-UITopic-0-0} {CallbackCapacityPlace-UITopic-0-0} {CallbackInputPlace-UITopic-0-0} -> {CallbackConnectorPlace-UITopic-0-0} +tr {CallbackOutputTransition-LeftCellTopic-0-0} {CallbackConnectorPlace-LeftCellTopic-0-0} -> {CallbackCapacityPlace-LeftCellTopic-0-0} {L-AwaitingControl} +tr {CallbackOutputTransition-UITopic-0-0} {CallbackConnectorPlace-UITopic-0-0} -> {CallbackCapacityPlace-UITopic-0-0} FeedbackIn +tr {CallbackOverflowTransition-LeftCellTopic-0-0} {CallbackCapacityPlace-LeftCellTopic-0-0}?-1 {CallbackInputPlace-LeftCellTopic-0-0} -> +tr {CallbackOverflowTransition-UITopic-0-0} {CallbackCapacityPlace-UITopic-0-0}?-1 {CallbackInputPlace-UITopic-0-0} -> +tr {ChannelConnectorTransition-LeftCellTopic} {ChannelConnectorPlace-LeftCellTopic} -> {DispatcherInputPlace-LeftCellTopic-0} +tr {ChannelConnectorTransition-UITopic} {ChannelConnectorPlace-UITopic} -> {DispatcherInputPlace-UITopic-0} +tr {DispatcherInputTransition-LeftCellTopic-0} {DispatcherCapacityPlace-LeftCellTopic-0} {DispatcherInputPlace-LeftCellTopic-0} -> {DispatcherConnectorPlace-LeftCellTopic-0} +tr {DispatcherInputTransition-UITopic-0} {DispatcherCapacityPlace-UITopic-0} {DispatcherInputPlace-UITopic-0} -> {DispatcherConnectorPlace-UITopic-0} +tr {DispatcherOutputTransition-LeftCellTopic-0} {DispatcherConnectorPlace-LeftCellTopic-0} -> {CallbackInputPlace-LeftCellTopic-0-0} {DispatcherCapacityPlace-LeftCellTopic-0} +tr {DispatcherOutputTransition-UITopic-0} {DispatcherConnectorPlace-UITopic-0} -> {CallbackInputPlace-UITopic-0-0} {DispatcherCapacityPlace-UITopic-0} +tr {DispatcherOverflowTransition-LeftCellTopic-0} {DispatcherCapacityPlace-LeftCellTopic-0}?-1 {DispatcherInputPlace-LeftCellTopic-0} -> +tr {DispatcherOverflowTransition-UITopic-0} {DispatcherCapacityPlace-UITopic-0}?-1 {DispatcherInputPlace-UITopic-0} -> +tr {End-INSTANCE-0} {EndControlIn-INSTANCE-0} -> GetShared {EndControlOut-INSTANCE-0} +tr {End-INSTANCE-1} {EndControlIn-INSTANCE-1} -> GetShared {EndControlOut-INSTANCE-1} +tr {Get-INSTANCE-0} GetShared {GetControlIn-INSTANCE-0} -> {GetControlOut-INSTANCE-0} +tr {Get-INSTANCE-1} GetShared {GetControlIn-INSTANCE-1} -> {GetControlOut-INSTANCE-1} +tr {GetSensorData-INSTANCE-0} {SensorIn-INSTANCE-0} {PD-0-GetSensorData-INSTANCE-0} -> {PD-0-GetSensorData-INSTANCE-0} {SensorInter-INSTANCE-0} +tr {InputSignalToFalseTransition-Blue} {PD-0-SortBlue} {InputSignalTruePlace-Blue} -> {InputSignalFalsePlace-Blue} +tr {InputSignalToFalseTransition-Green} {InputSignalTruePlace-Green} -> {InputSignalFalsePlace-Green} +tr {InputSignalToFalseTransition-PickFail} {InputSignalTruePlace-PickFail} {PD-0-PickingFail-INSTANCE-1} {PD-0-PickingFail-INSTANCE-0} -> {InputSignalFalsePlace-PickFail} +tr {InputSignalToFalseTransition-PickSuccess} {PD-0-PickingSuccess-INSTANCE-1} {InputSignalTruePlace-PickSuccess} {PD-0-PickingSuccess-INSTANCE-0} -> {InputSignalFalsePlace-PickSuccess} +tr {InputSignalToFalseTransition-PlaceFail} {InputSignalTruePlace-PlaceFail} {PD-0-PlacingFail-INSTANCE-0} {PD-0-PlacingFail-INSTANCE-1} -> {InputSignalFalsePlace-PlaceFail} +tr {InputSignalToFalseTransition-PlaceSuccess} {PD-0-PlacingSuccess-INSTANCE-0} {PD-0-PlacingSuccess-INSTANCE-1} {InputSignalTruePlace-PlaceSuccess} -> {InputSignalFalsePlace-PlaceSuccess} +tr {InputSignalToFalseTransition-Red} {InputSignalTruePlace-Red} {PD-0-SortRed} -> {InputSignalFalsePlace-Red} +tr {InputSignalToFalseTransition-Sensor} {PD-0-GetSensorData-INSTANCE-0} {InputSignalTruePlace-Sensor} -> {InputSignalFalsePlace-Sensor} +tr {InputSignalToFalseTransition-Stop} {PD-0-SafeToUnsafe} {InputSignalTruePlace-Stop} -> {InputSignalFalsePlace-Stop} +tr {InputSignalToTrueTransition-Blue} {InputSignalFalsePlace-Blue} -> {PD-0-SortBlue} {InputSignalTruePlace-Blue} +tr {InputSignalToTrueTransition-Green} {InputSignalFalsePlace-Green} -> {InputSignalTruePlace-Green} +tr {InputSignalToTrueTransition-PickFail} {InputSignalFalsePlace-PickFail} -> {InputSignalTruePlace-PickFail} {PD-0-PickingFail-INSTANCE-1} {PD-0-PickingFail-INSTANCE-0} +tr {InputSignalToTrueTransition-PickSuccess} {InputSignalFalsePlace-PickSuccess} -> {PD-0-PickingSuccess-INSTANCE-1} {InputSignalTruePlace-PickSuccess} {PD-0-PickingSuccess-INSTANCE-0} +tr {InputSignalToTrueTransition-PlaceFail} {InputSignalFalsePlace-PlaceFail} -> {InputSignalTruePlace-PlaceFail} {PD-0-PlacingFail-INSTANCE-0} {PD-0-PlacingFail-INSTANCE-1} +tr {InputSignalToTrueTransition-PlaceSuccess} {InputSignalFalsePlace-PlaceSuccess} -> {PD-0-PlacingSuccess-INSTANCE-0} {PD-0-PlacingSuccess-INSTANCE-1} {InputSignalTruePlace-PlaceSuccess} +tr {InputSignalToTrueTransition-Red} {InputSignalFalsePlace-Red} -> {InputSignalTruePlace-Red} {PD-0-SortRed} +tr {InputSignalToTrueTransition-Sensor} {InputSignalFalsePlace-Sensor} -> {PD-0-GetSensorData-INSTANCE-0} {InputSignalTruePlace-Sensor} +tr {InputSignalToTrueTransition-Stop} {InputSignalFalsePlace-Stop} -> {PD-0-SafeToUnsafe} {InputSignalTruePlace-Stop} +tr {Pick-INSTANCE-0} Safe {PickInput-INSTANCE-0} -> Safe {Picking-INSTANCE-0} +tr {Pick-INSTANCE-1} Safe {PickInput-INSTANCE-1} -> Safe {Picking-INSTANCE-1} +tr {PickingAbort-INSTANCE-0} {Picking-INSTANCE-0} Unsafe -> {PickOutput-INSTANCE-0} Unsafe +tr {PickingAbort-INSTANCE-1} {Picking-INSTANCE-1} Unsafe -> {PickOutput-INSTANCE-1} Unsafe +tr {PickingFail-INSTANCE-0} {PD-0-PickingFail-INSTANCE-0} {Picking-INSTANCE-0} -> {PD-0-PickingFail-INSTANCE-0} {PickOutput-INSTANCE-0} +tr {PickingFail-INSTANCE-1} {PD-0-PickingFail-INSTANCE-1} {Picking-INSTANCE-1} -> {PD-0-PickingFail-INSTANCE-1} {PickOutput-INSTANCE-1} +tr {PickingSuccess-INSTANCE-0} {PD-0-PickingSuccess-INSTANCE-0} {Picking-INSTANCE-0} -> {PD-0-PickingSuccess-INSTANCE-0} {PickOutput-INSTANCE-0} +tr {PickingSuccess-INSTANCE-1} {PD-0-PickingSuccess-INSTANCE-1} {Picking-INSTANCE-1} -> {PD-0-PickingSuccess-INSTANCE-1} {PickOutput-INSTANCE-1} +tr {Place-INSTANCE-0} Safe {PlaceInput-INSTANCE-0} -> Safe {Placing-INSTANCE-0} +tr {Place-INSTANCE-1} Safe {PlaceInput-INSTANCE-1} -> Safe {Placing-INSTANCE-1} +tr {PlacingAbort-INSTANCE-0} Unsafe {Placing-INSTANCE-0} -> Unsafe {PlaceOutput-INSTANCE-0} +tr {PlacingAbort-INSTANCE-1} Unsafe {Placing-INSTANCE-1} -> Unsafe {PlaceOutput-INSTANCE-1} +tr {PlacingFail-INSTANCE-0} {PD-0-PlacingFail-INSTANCE-0} {Placing-INSTANCE-0} -> {PD-0-PlacingFail-INSTANCE-0} {PlaceOutput-INSTANCE-0} +tr {PlacingFail-INSTANCE-1} {PD-0-PlacingFail-INSTANCE-1} {Placing-INSTANCE-1} -> {PD-0-PlacingFail-INSTANCE-1} {PlaceOutput-INSTANCE-1} +tr {PlacingSuccess-INSTANCE-0} {PD-0-PlacingSuccess-INSTANCE-0} {Placing-INSTANCE-0} -> {PD-0-PlacingSuccess-INSTANCE-0} {PlaceOutput-INSTANCE-0} +tr {PlacingSuccess-INSTANCE-1} {PD-0-PlacingSuccess-INSTANCE-1} {Placing-INSTANCE-1} -> {PD-0-PlacingSuccess-INSTANCE-1} {PlaceOutput-INSTANCE-1} +tr {ProcessSensorData-INSTANCE-0} {SensorInter-INSTANCE-0} -> {SensorOut-INSTANCE-0} +tr {PublisherInputTransition-LeftCellTopic-0} {PublisherCapacityPlace-LeftCellTopic-0} RedOut -> {PublisherConnectorPlace-LeftCellTopic-0} +tr {PublisherInputTransition-LeftCellTopic-1} BlueOut {PublisherCapacityPlace-LeftCellTopic-1} -> {PublisherConnectorPlace-LeftCellTopic-1} +tr {PublisherInputTransition-UITopic-0} {L-Done} {PublisherCapacityPlace-UITopic-0} -> {PublisherConnectorPlace-UITopic-0} +tr {PublisherOutputTransition-LeftCellTopic-0} {PublisherConnectorPlace-LeftCellTopic-0} -> {ChannelConnectorPlace-LeftCellTopic} {PublisherCapacityPlace-LeftCellTopic-0} +tr {PublisherOutputTransition-LeftCellTopic-1} {PublisherConnectorPlace-LeftCellTopic-1} -> {ChannelConnectorPlace-LeftCellTopic} {PublisherCapacityPlace-LeftCellTopic-1} +tr {PublisherOutputTransition-UITopic-0} {PublisherConnectorPlace-UITopic-0} -> {ChannelConnectorPlace-UITopic} {PublisherCapacityPlace-UITopic-0} +tr {PublisherOverflowTransition-LeftCellTopic-0} {PublisherCapacityPlace-LeftCellTopic-0}?-1 RedOut -> +tr {PublisherOverflowTransition-LeftCellTopic-1} BlueOut {PublisherCapacityPlace-LeftCellTopic-1}?-1 -> +tr {PublisherOverflowTransition-UITopic-0} {L-Done} {PublisherCapacityPlace-UITopic-0}?-1 -> +tr SafeToSensorCall Safe -> SensorCall +tr SafeToUnsafe {PD-0-SafeToUnsafe} Safe -> {PD-0-SafeToUnsafe} Unsafe +tr {ServiceCallMultiEntryTransition-endControlService-0-0} {ServiceClientCallPlace-endControlService-0} {ServiceCallMultiInactivePlace-endControlService-0} -> {EndControlIn-INSTANCE-0} {ServiceCallMultiActivePlace-endControlService-0} {ServiceCallMultiFlagPlace-endControlService-0-0} +tr {ServiceCallMultiEntryTransition-endControlService-1-0} {ServiceClientCallPlace-endControlService-0} {ServiceCallMultiInactivePlace-endControlService-1} -> {EndControlIn-INSTANCE-1} {ServiceCallMultiActivePlace-endControlService-1} {ServiceCallMultiFlagPlace-endControlService-1-0} +tr {ServiceCallMultiEntryTransition-getControlService-0-0} {ServiceClientCallPlace-getControlService-0} {ServiceCallMultiInactivePlace-getControlService-0} -> {GetControlIn-INSTANCE-0} {ServiceCallMultiActivePlace-getControlService-0} {ServiceCallMultiFlagPlace-getControlService-0-0} +tr {ServiceCallMultiEntryTransition-getControlService-1-0} {ServiceClientCallPlace-getControlService-0} {ServiceCallMultiInactivePlace-getControlService-1} -> {GetControlIn-INSTANCE-1} {ServiceCallMultiActivePlace-getControlService-1} {ServiceCallMultiFlagPlace-getControlService-1-0} +tr {ServiceCallMultiEntryTransition-pickService-0-0} {ServiceCallMultiInactivePlace-pickService-0} {ServiceClientCallPlace-pickService-0} -> {PickInput-INSTANCE-0} {ServiceCallMultiActivePlace-pickService-0} {ServiceCallMultiFlagPlace-pickService-0-0} +tr {ServiceCallMultiEntryTransition-pickService-1-0} {ServiceClientCallPlace-pickService-0} {ServiceCallMultiInactivePlace-pickService-1} -> {PickInput-INSTANCE-1} {ServiceCallMultiActivePlace-pickService-1} {ServiceCallMultiFlagPlace-pickService-1-0} +tr {ServiceCallMultiEntryTransition-placeService-0-0} {ServiceClientCallPlace-placeService-0} {ServiceCallMultiInactivePlace-placeService-0} -> {PlaceInput-INSTANCE-0} {ServiceCallMultiActivePlace-placeService-0} {ServiceCallMultiFlagPlace-placeService-0-0} +tr {ServiceCallMultiEntryTransition-placeService-1-0} {ServiceClientCallPlace-placeService-0} {ServiceCallMultiInactivePlace-placeService-1} -> {PlaceInput-INSTANCE-1} {ServiceCallMultiActivePlace-placeService-1} {ServiceCallMultiFlagPlace-placeService-1-0} +tr {ServiceCallMultiEntryTransition-sensorService-0-0} {ServiceCallMultiInactivePlace-sensorService-0} {ServiceClientCallPlace-sensorService-0} -> {SensorIn-INSTANCE-0} {ServiceCallMultiActivePlace-sensorService-0} {ServiceCallMultiFlagPlace-sensorService-0-0} +tr {ServiceCallMultiExitTransition-endControlService-0-0} {EndControlOut-INSTANCE-0} {ServiceCallMultiActivePlace-endControlService-0} {ServiceCallMultiFlagPlace-endControlService-0-0} -> {ServiceCallMultiInactivePlace-endControlService-0} {ServiceClientRespPlace-endControlService-0} +tr {ServiceCallMultiExitTransition-endControlService-1-0} {EndControlOut-INSTANCE-1} {ServiceCallMultiActivePlace-endControlService-1} {ServiceCallMultiFlagPlace-endControlService-1-0} -> {ServiceCallMultiInactivePlace-endControlService-1} {ServiceClientRespPlace-endControlService-0} +tr {ServiceCallMultiExitTransition-getControlService-0-0} {GetControlOut-INSTANCE-0} {ServiceCallMultiActivePlace-getControlService-0} {ServiceCallMultiFlagPlace-getControlService-0-0} -> {ServiceCallMultiInactivePlace-getControlService-0} {ServiceClientRespPlace-getControlService-0} +tr {ServiceCallMultiExitTransition-getControlService-1-0} {GetControlOut-INSTANCE-1} {ServiceCallMultiActivePlace-getControlService-1} {ServiceCallMultiFlagPlace-getControlService-1-0} -> {ServiceCallMultiInactivePlace-getControlService-1} {ServiceClientRespPlace-getControlService-0} +tr {ServiceCallMultiExitTransition-pickService-0-0} {PickOutput-INSTANCE-0} {ServiceCallMultiActivePlace-pickService-0} {ServiceCallMultiFlagPlace-pickService-0-0} -> {ServiceCallMultiInactivePlace-pickService-0} {ServiceClientRespPlace-pickService-0} +tr {ServiceCallMultiExitTransition-pickService-1-0} {PickOutput-INSTANCE-1} {ServiceCallMultiActivePlace-pickService-1} {ServiceCallMultiFlagPlace-pickService-1-0} -> {ServiceCallMultiInactivePlace-pickService-1} {ServiceClientRespPlace-pickService-0} +tr {ServiceCallMultiExitTransition-placeService-0-0} {PlaceOutput-INSTANCE-0} {ServiceCallMultiActivePlace-placeService-0} {ServiceCallMultiFlagPlace-placeService-0-0} -> {ServiceCallMultiInactivePlace-placeService-0} {ServiceClientRespPlace-placeService-0} +tr {ServiceCallMultiExitTransition-placeService-1-0} {PlaceOutput-INSTANCE-1} {ServiceCallMultiActivePlace-placeService-1} {ServiceCallMultiFlagPlace-placeService-1-0} -> {ServiceCallMultiInactivePlace-placeService-1} {ServiceClientRespPlace-placeService-0} +tr {ServiceCallMultiExitTransition-sensorService-0-0} {SensorOut-INSTANCE-0} {ServiceCallMultiActivePlace-sensorService-0} {ServiceCallMultiFlagPlace-sensorService-0-0} -> {ServiceCallMultiInactivePlace-sensorService-0} {ServiceClientRespPlace-sensorService-0} +tr {ServiceClientCallConnectTransition-endControlService-0} {L-ObjectPlaced} {ServiceTogglePlace-endControlService-0} -> {ServiceClientCallConnectPlace-endControlService-0} +tr {ServiceClientCallConnectTransition-getControlService-0} {L-AwaitingControl} {ServiceTogglePlace-getControlService-0} -> {ServiceClientCallConnectPlace-getControlService-0} +tr {ServiceClientCallConnectTransition-pickService-0} {L-Ready} {ServiceTogglePlace-pickService-0} -> {ServiceClientCallConnectPlace-pickService-0} +tr {ServiceClientCallConnectTransition-placeService-0} {L-ObjectPicked} {ServiceTogglePlace-placeService-0} -> {ServiceClientCallConnectPlace-placeService-0} +tr {ServiceClientCallConnectTransition-sensorService-0} SensorCall {ServiceTogglePlace-sensorService-0} -> {ServiceClientCallConnectPlace-sensorService-0} +tr {ServiceClientCallTransition-endControlService-0} {ServiceClientCallConnectPlace-endControlService-0} -> {ServiceClientCallPlace-endControlService-0} +tr {ServiceClientCallTransition-getControlService-0} {ServiceClientCallConnectPlace-getControlService-0} -> {ServiceClientCallPlace-getControlService-0} +tr {ServiceClientCallTransition-pickService-0} {ServiceClientCallConnectPlace-pickService-0} -> {ServiceClientCallPlace-pickService-0} +tr {ServiceClientCallTransition-placeService-0} {ServiceClientCallConnectPlace-placeService-0} -> {ServiceClientCallPlace-placeService-0} +tr {ServiceClientCallTransition-sensorService-0} {ServiceClientCallConnectPlace-sensorService-0} -> {ServiceClientCallPlace-sensorService-0} +tr {ServiceClientRespConnectTransition-endControlService-0} {ServiceClientRespConnectPlace-endControlService-0} -> {L-Done} {ServiceTogglePlace-endControlService-0} +tr {ServiceClientRespConnectTransition-getControlService-0} {ServiceClientRespConnectPlace-getControlService-0} -> {L-Ready} {ServiceTogglePlace-getControlService-0} +tr {ServiceClientRespConnectTransition-pickService-0} {ServiceClientRespConnectPlace-pickService-0} -> {L-ObjectPicked} {ServiceTogglePlace-pickService-0} +tr {ServiceClientRespConnectTransition-placeService-0} {ServiceClientRespConnectPlace-placeService-0} -> {L-ObjectPlaced} {ServiceTogglePlace-placeService-0} +tr {ServiceClientRespConnectTransition-sensorService-0} {ServiceClientRespConnectPlace-sensorService-0} -> SensorResponse {ServiceTogglePlace-sensorService-0} +tr {ServiceClientRespTransition-endControlService-0} {ServiceClientRespPlace-endControlService-0} -> {ServiceClientRespConnectPlace-endControlService-0} +tr {ServiceClientRespTransition-getControlService-0} {ServiceClientRespPlace-getControlService-0} -> {ServiceClientRespConnectPlace-getControlService-0} +tr {ServiceClientRespTransition-pickService-0} {ServiceClientRespPlace-pickService-0} -> {ServiceClientRespConnectPlace-pickService-0} +tr {ServiceClientRespTransition-placeService-0} {ServiceClientRespPlace-placeService-0} -> {ServiceClientRespConnectPlace-placeService-0} +tr {ServiceClientRespTransition-sensorService-0} {ServiceClientRespPlace-sensorService-0} -> {ServiceClientRespConnectPlace-sensorService-0} +tr ShowFeedback FeedbackIn -> FeedbackDone +tr SortBlue {PD-0-SortBlue} ObjectPoolBlue -> BlueOut {PD-0-SortBlue} +tr SortRed {PD-0-SortRed} ObjectPoolRed -> {PD-0-SortRed} RedOut +tr TransitionSafe SensorResponse -> Safe +tr TransitionUnsafe SensorResponse -> Unsafe +tr UnsafeToSensorCall Unsafe -> SensorCall +pl {CallbackCapacityPlace-LeftCellTopic-0-0} (10) +pl {CallbackCapacityPlace-UITopic-0-0} (10) +pl {DispatcherCapacityPlace-LeftCellTopic-0} (16) +pl {DispatcherCapacityPlace-UITopic-0} (16) +pl GetShared (1) +pl {InputSignalFalsePlace-Blue} (1) +pl {InputSignalFalsePlace-Green} (1) +pl {InputSignalFalsePlace-PickFail} (1) +pl {InputSignalFalsePlace-PickSuccess} (1) +pl {InputSignalFalsePlace-PlaceFail} (1) +pl {InputSignalFalsePlace-PlaceSuccess} (1) +pl {InputSignalFalsePlace-Red} (1) +pl {InputSignalFalsePlace-Sensor} (1) +pl {InputSignalFalsePlace-Stop} (1) +pl ObjectPoolBlue (1) +pl ObjectPoolRed (1) +pl {PublisherCapacityPlace-LeftCellTopic-0} (10) +pl {PublisherCapacityPlace-LeftCellTopic-1} (10) +pl {PublisherCapacityPlace-UITopic-0} (10) +pl {ServiceCallMultiInactivePlace-endControlService-0} (1) +pl {ServiceCallMultiInactivePlace-endControlService-1} (1) +pl {ServiceCallMultiInactivePlace-getControlService-0} (1) +pl {ServiceCallMultiInactivePlace-getControlService-1} (1) +pl {ServiceCallMultiInactivePlace-pickService-0} (1) +pl {ServiceCallMultiInactivePlace-pickService-1} (1) +pl {ServiceCallMultiInactivePlace-placeService-0} (1) +pl {ServiceCallMultiInactivePlace-placeService-1} (1) +pl {ServiceCallMultiInactivePlace-sensorService-0} (1) +pl {ServiceTogglePlace-endControlService-0} (1) +pl {ServiceTogglePlace-getControlService-0} (1) +pl {ServiceTogglePlace-pickService-0} (1) +pl {ServiceTogglePlace-placeService-0} (1) +pl {ServiceTogglePlace-sensorService-0} (1) +pl Unsafe (1) diff --git a/models/task-2/model-one-robot.pnml b/models/task-2/model-one-robot.pnml index 2a84101..685ea4f 100644 --- a/models/task-2/model-one-robot.pnml +++ b/models/task-2/model-one-robot.pnml @@ -85,25 +85,7 @@ <text>ObjectPoolBlue</text> </name> </place> - <place id="ObjectPoolGreen"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>selector</node> - <subnet>selectorGreen</subnet> - <balloonMarking> - <tokens> - <token>{"color" : "red", "name" : "red1", "pickSuccess" : "false", "placeSuccess" : "false", - "humanDetected" : "false", "sensorData" : "", "trace" : "", "locked" : "false" } </token> - </tokens> - </balloonMarking> - </toolspecific> - <initialMarking> - <text>1</text> - </initialMarking> - <name> - <text>ObjectPoolGreen</text> - </name> - </place> - + <transition id="SortRed"> <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> <node>selector</node> @@ -126,17 +108,6 @@ <text>SortBlue</text> </name> </transition> - <transition id="SortGreen"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>selector</node> - <subnet>selectorGreen</subnet> - <type>discreteTransitionType</type> - <inputsignalclause>(Green)</inputsignalclause> - </toolspecific> - <name> - <text>SortGreen</text> - </name> - </transition> <place id="RedOut"> <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> @@ -156,28 +127,15 @@ <text>BlueOut</text> </name> </place> - <place id="GreenOut"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>selector</node> - <subnet>selectorGreen</subnet> - </toolspecific> - <name> - <text>GreenOut</text> - </name> - </place> <arc id="a1" source="SortRed" target="RedOut"> </arc> <arc id="a2" source="SortBlue" target="BlueOut"> </arc> - <arc id="a3" source="SortGreen" target="GreenOut"> - </arc> <arc id="a4" source="ObjectPoolRed" target="SortRed"> </arc> <arc id="a5" source="ObjectPoolBlue" target="SortBlue"> </arc> - <arc id="a6" source="ObjectPoolGreen" target="SortGreen"> - </arc> </page> <transition id="LeftCellTopic"> @@ -205,27 +163,6 @@ <text>LeftCellTopic</text> </name> </transition> - <transition id="RightCellTopic"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <type>topicTransitionType</type> - <topicName>RightCellTopic</topicName> - <publishers> - <publisher> - <id>GreenOut</id> - <limit>10</limit> - </publisher> - </publishers> - <subscribers> - <subscriber> - <id>R-AwaitingControl</id> - <limit>10</limit> - </subscriber> - </subscribers> - </toolspecific> - <name> - <text>RightCellTopic</text> - </name> - </transition> <transition id="UITopic"> <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> @@ -236,10 +173,6 @@ <id>L-Done</id> <limit>10</limit> </publisher> - <publisher> - <id>R-Done</id> - <limit>10</limit> - </publisher> </publishers> <subscribers> <subscriber> @@ -305,58 +238,6 @@ </place> </page> - <page id="RightControllerPage"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <type>nodePage</type> - </toolspecific> - - <place id="R-AwaitingControl"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>RightController</node> - <subnet>RC1</subnet> - </toolspecific> - <name> - <text>R-AwaitingControl</text> - </name> - </place> - <place id="R-Ready"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>RightController</node> - <subnet>RC1</subnet> - </toolspecific> - <name> - <text>R-Ready</text> - </name> - </place> - <place id="R-ObjectPicked"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>RightController</node> - <subnet>RC1</subnet> - </toolspecific> - <name> - <text>R-ObjectPicked</text> - </name> - </place> - <place id="R-ObjectPlaced"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>RightController</node> - <subnet>RC1</subnet> - </toolspecific> - <name> - <text>R-ObjectPlaced</text> - </name> - </place> - <place id="R-Done"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>RightController</node> - <subnet>RC1</subnet> - </toolspecific> - <name> - <text>R-Done</text> - </name> - </place> - </page> - <page id="FeedbackPage"> <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> <type>nodePage</type> @@ -541,11 +422,6 @@ <request>L-AwaitingControl</request> <response>L-Ready</response> </channel> - <channel> - <cid>c2</cid> - <request>R-AwaitingControl</request> - <response>R-Ready</response> - </channel> </channels> </toolspecific> <name> @@ -565,11 +441,6 @@ <request>L-ObjectPlaced</request> <response>L-Done</response> </channel> - <channel> - <cid>c4</cid> - <request>R-ObjectPlaced</request> - <response>R-Done</response> - </channel> </channels> </toolspecific> <name> @@ -590,11 +461,6 @@ <request>L-Ready</request> <response>L-ObjectPicked</response> </channel> - <channel> - <cid>c6</cid> - <request>R-Ready</request> - <response>R-ObjectPicked</response> - </channel> </channels> </toolspecific> <name> @@ -615,11 +481,6 @@ <request>L-ObjectPicked</request> <response>L-ObjectPlaced</response> </channel> - <channel> - <cid>c8</cid> - <request>R-ObjectPicked</request> - <response>R-ObjectPlaced</response> - </channel> </channels> </toolspecific> <name> diff --git a/models/task-2/model-without-sync-flatted.net b/models/task-2/model-without-sync-flatted.net new file mode 100644 index 0000000..6fc8756 --- /dev/null +++ b/models/task-2/model-without-sync-flatted.net @@ -0,0 +1,158 @@ +net FullModel +tr {CallbackInputTransition-LeftCellTopic-0-0} {CallbackCapacityPlace-LeftCellTopic-0-0} {CallbackInputPlace-LeftCellTopic-0-0} -> {CallbackConnectorPlace-LeftCellTopic-0-0} +tr {CallbackInputTransition-RightCellTopic-0-0} {CallbackCapacityPlace-RightCellTopic-0-0} {CallbackInputPlace-RightCellTopic-0-0} -> {CallbackConnectorPlace-RightCellTopic-0-0} +tr {CallbackInputTransition-UITopic-0-0} {CallbackCapacityPlace-UITopic-0-0} {CallbackInputPlace-UITopic-0-0} -> {CallbackConnectorPlace-UITopic-0-0} +tr {CallbackOutputTransition-LeftCellTopic-0-0} {CallbackConnectorPlace-LeftCellTopic-0-0} -> {CallbackCapacityPlace-LeftCellTopic-0-0} {L-AwaitingControl} +tr {CallbackOutputTransition-RightCellTopic-0-0} {CallbackConnectorPlace-RightCellTopic-0-0} -> {CallbackCapacityPlace-RightCellTopic-0-0} {R-AwaitingControl} +tr {CallbackOutputTransition-UITopic-0-0} {CallbackConnectorPlace-UITopic-0-0} -> {CallbackCapacityPlace-UITopic-0-0} FeedbackIn +tr {CallbackOverflowTransition-LeftCellTopic-0-0} {CallbackCapacityPlace-LeftCellTopic-0-0}?-1 {CallbackInputPlace-LeftCellTopic-0-0} -> +tr {CallbackOverflowTransition-RightCellTopic-0-0} {CallbackCapacityPlace-RightCellTopic-0-0}?-1 {CallbackInputPlace-RightCellTopic-0-0} -> +tr {CallbackOverflowTransition-UITopic-0-0} {CallbackCapacityPlace-UITopic-0-0}?-1 {CallbackInputPlace-UITopic-0-0} -> +tr {ChannelConnectorTransition-LeftCellTopic} {ChannelConnectorPlace-LeftCellTopic} -> {DispatcherInputPlace-LeftCellTopic-0} +tr {ChannelConnectorTransition-RightCellTopic} {ChannelConnectorPlace-RightCellTopic} -> {DispatcherInputPlace-RightCellTopic-0} +tr {ChannelConnectorTransition-UITopic} {ChannelConnectorPlace-UITopic} -> {DispatcherInputPlace-UITopic-0} +tr {DispatcherInputTransition-LeftCellTopic-0} {DispatcherCapacityPlace-LeftCellTopic-0} {DispatcherInputPlace-LeftCellTopic-0} -> {DispatcherConnectorPlace-LeftCellTopic-0} +tr {DispatcherInputTransition-RightCellTopic-0} {DispatcherCapacityPlace-RightCellTopic-0} {DispatcherInputPlace-RightCellTopic-0} -> {DispatcherConnectorPlace-RightCellTopic-0} +tr {DispatcherInputTransition-UITopic-0} {DispatcherCapacityPlace-UITopic-0} {DispatcherInputPlace-UITopic-0} -> {DispatcherConnectorPlace-UITopic-0} +tr {DispatcherOutputTransition-LeftCellTopic-0} {DispatcherConnectorPlace-LeftCellTopic-0} -> {CallbackInputPlace-LeftCellTopic-0-0} {DispatcherCapacityPlace-LeftCellTopic-0} +tr {DispatcherOutputTransition-RightCellTopic-0} {DispatcherConnectorPlace-RightCellTopic-0} -> {CallbackInputPlace-RightCellTopic-0-0} {DispatcherCapacityPlace-RightCellTopic-0} +tr {DispatcherOutputTransition-UITopic-0} {DispatcherConnectorPlace-UITopic-0} -> {CallbackInputPlace-UITopic-0-0} {DispatcherCapacityPlace-UITopic-0} +tr {DispatcherOverflowTransition-LeftCellTopic-0} {DispatcherCapacityPlace-LeftCellTopic-0}?-1 {DispatcherInputPlace-LeftCellTopic-0} -> +tr {DispatcherOverflowTransition-RightCellTopic-0} {DispatcherCapacityPlace-RightCellTopic-0}?-1 {DispatcherInputPlace-RightCellTopic-0} -> +tr {DispatcherOverflowTransition-UITopic-0} {DispatcherCapacityPlace-UITopic-0}?-1 {DispatcherInputPlace-UITopic-0} -> +tr {GetSensorData-INSTANCE-0} {PD-0-GetSensorData-INSTANCE-0} {SensorIn-INSTANCE-0} -> {PD-0-GetSensorData-INSTANCE-0} {SensorInter-INSTANCE-0} +tr {InputSignalToFalseTransition-Blue} {InputSignalTruePlace-Blue} {PD-0-SortBlue} -> {InputSignalFalsePlace-Blue} +tr {InputSignalToFalseTransition-Green} {InputSignalTruePlace-Green} {PD-0-SortGreen} -> {InputSignalFalsePlace-Green} +tr {InputSignalToFalseTransition-PickFail} {PD-0-PickingFail-INSTANCE-0} {PD-0-PickingFail-INSTANCE-1} {InputSignalTruePlace-PickFail} -> {InputSignalFalsePlace-PickFail} +tr {InputSignalToFalseTransition-PickSuccess} {InputSignalTruePlace-PickSuccess} {PD-0-PickingSuccess-INSTANCE-1} {PD-0-PickingSuccess-INSTANCE-0} -> {InputSignalFalsePlace-PickSuccess} +tr {InputSignalToFalseTransition-PlaceFail} {InputSignalTruePlace-PlaceFail} {PD-0-PlacingFail-INSTANCE-0} {PD-0-PlacingFail-INSTANCE-1} -> {InputSignalFalsePlace-PlaceFail} +tr {InputSignalToFalseTransition-PlaceSuccess} {PD-0-PlacingSuccess-INSTANCE-1} {PD-0-PlacingSuccess-INSTANCE-0} {InputSignalTruePlace-PlaceSuccess} -> {InputSignalFalsePlace-PlaceSuccess} +tr {InputSignalToFalseTransition-Red} {InputSignalTruePlace-Red} {PD-0-SortRed} -> {InputSignalFalsePlace-Red} +tr {InputSignalToFalseTransition-Sensor} {PD-0-GetSensorData-INSTANCE-0} {InputSignalTruePlace-Sensor} -> {InputSignalFalsePlace-Sensor} +tr {InputSignalToFalseTransition-Stop} {PD-0-SafeToUnsafe} {InputSignalTruePlace-Stop} -> {InputSignalFalsePlace-Stop} +tr {InputSignalToTrueTransition-Blue} {InputSignalFalsePlace-Blue} -> {InputSignalTruePlace-Blue} {PD-0-SortBlue} +tr {InputSignalToTrueTransition-Green} {InputSignalFalsePlace-Green} -> {InputSignalTruePlace-Green} {PD-0-SortGreen} +tr {InputSignalToTrueTransition-PickFail} {InputSignalFalsePlace-PickFail} -> {PD-0-PickingFail-INSTANCE-0} {PD-0-PickingFail-INSTANCE-1} {InputSignalTruePlace-PickFail} +tr {InputSignalToTrueTransition-PickSuccess} {InputSignalFalsePlace-PickSuccess} -> {InputSignalTruePlace-PickSuccess} {PD-0-PickingSuccess-INSTANCE-1} {PD-0-PickingSuccess-INSTANCE-0} +tr {InputSignalToTrueTransition-PlaceFail} {InputSignalFalsePlace-PlaceFail} -> {InputSignalTruePlace-PlaceFail} {PD-0-PlacingFail-INSTANCE-0} {PD-0-PlacingFail-INSTANCE-1} +tr {InputSignalToTrueTransition-PlaceSuccess} {InputSignalFalsePlace-PlaceSuccess} -> {PD-0-PlacingSuccess-INSTANCE-1} {PD-0-PlacingSuccess-INSTANCE-0} {InputSignalTruePlace-PlaceSuccess} +tr {InputSignalToTrueTransition-Red} {InputSignalFalsePlace-Red} -> {InputSignalTruePlace-Red} {PD-0-SortRed} +tr {InputSignalToTrueTransition-Sensor} {InputSignalFalsePlace-Sensor} -> {PD-0-GetSensorData-INSTANCE-0} {InputSignalTruePlace-Sensor} +tr {InputSignalToTrueTransition-Stop} {InputSignalFalsePlace-Stop} -> {PD-0-SafeToUnsafe} {InputSignalTruePlace-Stop} +tr {L-EndControl-T} {L-ObjectPlaced} -> {L-Done} +tr {L-ReqControl-T} {L-AwaitingControl} -> {L-Ready} +tr {Pick-INSTANCE-0} Safe {PickInput-INSTANCE-0} -> Safe {Picking-INSTANCE-0} +tr {Pick-INSTANCE-1} Safe {PickInput-INSTANCE-1} -> Safe {Picking-INSTANCE-1} +tr {PickingAbort-INSTANCE-0} {Picking-INSTANCE-0} Unsafe -> {PickOutput-INSTANCE-0} Unsafe +tr {PickingAbort-INSTANCE-1} {Picking-INSTANCE-1} Unsafe -> {PickOutput-INSTANCE-1} Unsafe +tr {PickingFail-INSTANCE-0} {PD-0-PickingFail-INSTANCE-0} {Picking-INSTANCE-0} -> {PD-0-PickingFail-INSTANCE-0} {PickOutput-INSTANCE-0} +tr {PickingFail-INSTANCE-1} {PD-0-PickingFail-INSTANCE-1} {Picking-INSTANCE-1} -> {PD-0-PickingFail-INSTANCE-1} {PickOutput-INSTANCE-1} +tr {PickingSuccess-INSTANCE-0} {PD-0-PickingSuccess-INSTANCE-0} {Picking-INSTANCE-0} -> {PD-0-PickingSuccess-INSTANCE-0} {PickOutput-INSTANCE-0} +tr {PickingSuccess-INSTANCE-1} {PD-0-PickingSuccess-INSTANCE-1} {Picking-INSTANCE-1} -> {PD-0-PickingSuccess-INSTANCE-1} {PickOutput-INSTANCE-1} +tr {Place-INSTANCE-0} Safe {PlaceInput-INSTANCE-0} -> Safe {Placing-INSTANCE-0} +tr {Place-INSTANCE-1} Safe {PlaceInput-INSTANCE-1} -> Safe {Placing-INSTANCE-1} +tr {PlacingAbort-INSTANCE-0} Unsafe {Placing-INSTANCE-0} -> Unsafe {PlaceOutput-INSTANCE-0} +tr {PlacingAbort-INSTANCE-1} Unsafe {Placing-INSTANCE-1} -> Unsafe {PlaceOutput-INSTANCE-1} +tr {PlacingFail-INSTANCE-0} {PD-0-PlacingFail-INSTANCE-0} {Placing-INSTANCE-0} -> {PD-0-PlacingFail-INSTANCE-0} {PlaceOutput-INSTANCE-0} +tr {PlacingFail-INSTANCE-1} {PD-0-PlacingFail-INSTANCE-1} {Placing-INSTANCE-1} -> {PD-0-PlacingFail-INSTANCE-1} {PlaceOutput-INSTANCE-1} +tr {PlacingSuccess-INSTANCE-0} {PD-0-PlacingSuccess-INSTANCE-0} {Placing-INSTANCE-0} -> {PD-0-PlacingSuccess-INSTANCE-0} {PlaceOutput-INSTANCE-0} +tr {PlacingSuccess-INSTANCE-1} {PD-0-PlacingSuccess-INSTANCE-1} {Placing-INSTANCE-1} -> {PD-0-PlacingSuccess-INSTANCE-1} {PlaceOutput-INSTANCE-1} +tr {ProcessSensorData-INSTANCE-0} {SensorInter-INSTANCE-0} -> {SensorOut-INSTANCE-0} +tr {PublisherInputTransition-LeftCellTopic-0} {PublisherCapacityPlace-LeftCellTopic-0} RedOut -> {PublisherConnectorPlace-LeftCellTopic-0} +tr {PublisherInputTransition-LeftCellTopic-1} BlueOut {PublisherCapacityPlace-LeftCellTopic-1} -> {PublisherConnectorPlace-LeftCellTopic-1} +tr {PublisherInputTransition-RightCellTopic-0} GreenOut {PublisherCapacityPlace-RightCellTopic-0} -> {PublisherConnectorPlace-RightCellTopic-0} +tr {PublisherInputTransition-UITopic-0} {L-Done} {PublisherCapacityPlace-UITopic-0} -> {PublisherConnectorPlace-UITopic-0} +tr {PublisherInputTransition-UITopic-1} {PublisherCapacityPlace-UITopic-1} {R-Done} -> {PublisherConnectorPlace-UITopic-1} +tr {PublisherOutputTransition-LeftCellTopic-0} {PublisherConnectorPlace-LeftCellTopic-0} -> {ChannelConnectorPlace-LeftCellTopic} {PublisherCapacityPlace-LeftCellTopic-0} +tr {PublisherOutputTransition-LeftCellTopic-1} {PublisherConnectorPlace-LeftCellTopic-1} -> {ChannelConnectorPlace-LeftCellTopic} {PublisherCapacityPlace-LeftCellTopic-1} +tr {PublisherOutputTransition-RightCellTopic-0} {PublisherConnectorPlace-RightCellTopic-0} -> {ChannelConnectorPlace-RightCellTopic} {PublisherCapacityPlace-RightCellTopic-0} +tr {PublisherOutputTransition-UITopic-0} {PublisherConnectorPlace-UITopic-0} -> {ChannelConnectorPlace-UITopic} {PublisherCapacityPlace-UITopic-0} +tr {PublisherOutputTransition-UITopic-1} {PublisherConnectorPlace-UITopic-1} -> {ChannelConnectorPlace-UITopic} {PublisherCapacityPlace-UITopic-1} +tr {PublisherOverflowTransition-LeftCellTopic-0} {PublisherCapacityPlace-LeftCellTopic-0}?-1 RedOut -> +tr {PublisherOverflowTransition-LeftCellTopic-1} BlueOut {PublisherCapacityPlace-LeftCellTopic-1}?-1 -> +tr {PublisherOverflowTransition-RightCellTopic-0} GreenOut {PublisherCapacityPlace-RightCellTopic-0}?-1 -> +tr {PublisherOverflowTransition-UITopic-0} {L-Done} {PublisherCapacityPlace-UITopic-0}?-1 -> +tr {PublisherOverflowTransition-UITopic-1} {PublisherCapacityPlace-UITopic-1}?-1 {R-Done} -> +tr {R-EndControl-T} {R-ObjectPlaced} -> {R-Done} +tr {R-ReqControl-T} {R-AwaitingControl} -> {R-Ready} +tr SafeToSensorCall Safe -> SensorCall +tr SafeToUnsafe {PD-0-SafeToUnsafe} Safe -> {PD-0-SafeToUnsafe} Unsafe +tr {ServiceCallMultiEntryTransition-pickService-0-0} {ServiceClientCallPlace-pickService-0} {ServiceCallMultiInactivePlace-pickService-0} -> {PickInput-INSTANCE-0} {ServiceCallMultiActivePlace-pickService-0} {ServiceCallMultiFlagPlace-pickService-0-0} +tr {ServiceCallMultiEntryTransition-pickService-0-1} {ServiceCallMultiInactivePlace-pickService-0} {ServiceClientCallPlace-pickService-1} -> {PickInput-INSTANCE-0} {ServiceCallMultiActivePlace-pickService-0} {ServiceCallMultiFlagPlace-pickService-0-1} +tr {ServiceCallMultiEntryTransition-pickService-1-0} {ServiceClientCallPlace-pickService-0} {ServiceCallMultiInactivePlace-pickService-1} -> {PickInput-INSTANCE-1} {ServiceCallMultiActivePlace-pickService-1} {ServiceCallMultiFlagPlace-pickService-1-0} +tr {ServiceCallMultiEntryTransition-pickService-1-1} {ServiceClientCallPlace-pickService-1} {ServiceCallMultiInactivePlace-pickService-1} -> {PickInput-INSTANCE-1} {ServiceCallMultiActivePlace-pickService-1} {ServiceCallMultiFlagPlace-pickService-1-1} +tr {ServiceCallMultiEntryTransition-placeService-0-0} {ServiceClientCallPlace-placeService-0} {ServiceCallMultiInactivePlace-placeService-0} -> {PlaceInput-INSTANCE-0} {ServiceCallMultiActivePlace-placeService-0} {ServiceCallMultiFlagPlace-placeService-0-0} +tr {ServiceCallMultiEntryTransition-placeService-0-1} {ServiceCallMultiInactivePlace-placeService-0} {ServiceClientCallPlace-placeService-1} -> {PlaceInput-INSTANCE-0} {ServiceCallMultiActivePlace-placeService-0} {ServiceCallMultiFlagPlace-placeService-0-1} +tr {ServiceCallMultiEntryTransition-placeService-1-0} {ServiceClientCallPlace-placeService-0} {ServiceCallMultiInactivePlace-placeService-1} -> {PlaceInput-INSTANCE-1} {ServiceCallMultiActivePlace-placeService-1} {ServiceCallMultiFlagPlace-placeService-1-0} +tr {ServiceCallMultiEntryTransition-placeService-1-1} {ServiceClientCallPlace-placeService-1} {ServiceCallMultiInactivePlace-placeService-1} -> {PlaceInput-INSTANCE-1} {ServiceCallMultiActivePlace-placeService-1} {ServiceCallMultiFlagPlace-placeService-1-1} +tr {ServiceCallMultiEntryTransition-sensorService-0-0} {ServiceCallMultiInactivePlace-sensorService-0} {ServiceClientCallPlace-sensorService-0} -> {SensorIn-INSTANCE-0} {ServiceCallMultiActivePlace-sensorService-0} {ServiceCallMultiFlagPlace-sensorService-0-0} +tr {ServiceCallMultiExitTransition-pickService-0-0} {PickOutput-INSTANCE-0} {ServiceCallMultiActivePlace-pickService-0} {ServiceCallMultiFlagPlace-pickService-0-0} -> {ServiceCallMultiInactivePlace-pickService-0} {ServiceClientRespPlace-pickService-0} +tr {ServiceCallMultiExitTransition-pickService-0-1} {PickOutput-INSTANCE-0} {ServiceCallMultiActivePlace-pickService-0} {ServiceCallMultiFlagPlace-pickService-0-1} -> {ServiceCallMultiInactivePlace-pickService-0} {ServiceClientRespPlace-pickService-1} +tr {ServiceCallMultiExitTransition-pickService-1-0} {PickOutput-INSTANCE-1} {ServiceCallMultiActivePlace-pickService-1} {ServiceCallMultiFlagPlace-pickService-1-0} -> {ServiceCallMultiInactivePlace-pickService-1} {ServiceClientRespPlace-pickService-0} +tr {ServiceCallMultiExitTransition-pickService-1-1} {PickOutput-INSTANCE-1} {ServiceCallMultiActivePlace-pickService-1} {ServiceCallMultiFlagPlace-pickService-1-1} -> {ServiceCallMultiInactivePlace-pickService-1} {ServiceClientRespPlace-pickService-1} +tr {ServiceCallMultiExitTransition-placeService-0-0} {PlaceOutput-INSTANCE-0} {ServiceCallMultiActivePlace-placeService-0} {ServiceCallMultiFlagPlace-placeService-0-0} -> {ServiceCallMultiInactivePlace-placeService-0} {ServiceClientRespPlace-placeService-0} +tr {ServiceCallMultiExitTransition-placeService-0-1} {PlaceOutput-INSTANCE-0} {ServiceCallMultiActivePlace-placeService-0} {ServiceCallMultiFlagPlace-placeService-0-1} -> {ServiceCallMultiInactivePlace-placeService-0} {ServiceClientRespPlace-placeService-1} +tr {ServiceCallMultiExitTransition-placeService-1-0} {PlaceOutput-INSTANCE-1} {ServiceCallMultiActivePlace-placeService-1} {ServiceCallMultiFlagPlace-placeService-1-0} -> {ServiceCallMultiInactivePlace-placeService-1} {ServiceClientRespPlace-placeService-0} +tr {ServiceCallMultiExitTransition-placeService-1-1} {PlaceOutput-INSTANCE-1} {ServiceCallMultiActivePlace-placeService-1} {ServiceCallMultiFlagPlace-placeService-1-1} -> {ServiceCallMultiInactivePlace-placeService-1} {ServiceClientRespPlace-placeService-1} +tr {ServiceCallMultiExitTransition-sensorService-0-0} {SensorOut-INSTANCE-0} {ServiceCallMultiActivePlace-sensorService-0} {ServiceCallMultiFlagPlace-sensorService-0-0} -> {ServiceCallMultiInactivePlace-sensorService-0} {ServiceClientRespPlace-sensorService-0} +tr {ServiceClientCallConnectTransition-pickService-0} {L-Ready} {ServiceTogglePlace-pickService-0} -> {ServiceClientCallConnectPlace-pickService-0} +tr {ServiceClientCallConnectTransition-pickService-1} {R-Ready} {ServiceTogglePlace-pickService-1} -> {ServiceClientCallConnectPlace-pickService-1} +tr {ServiceClientCallConnectTransition-placeService-0} {L-ObjectPicked} {ServiceTogglePlace-placeService-0} -> {ServiceClientCallConnectPlace-placeService-0} +tr {ServiceClientCallConnectTransition-placeService-1} {R-ObjectPicked} {ServiceTogglePlace-placeService-1} -> {ServiceClientCallConnectPlace-placeService-1} +tr {ServiceClientCallConnectTransition-sensorService-0} SensorCall {ServiceTogglePlace-sensorService-0} -> {ServiceClientCallConnectPlace-sensorService-0} +tr {ServiceClientCallTransition-pickService-0} {ServiceClientCallConnectPlace-pickService-0} -> {ServiceClientCallPlace-pickService-0} +tr {ServiceClientCallTransition-pickService-1} {ServiceClientCallConnectPlace-pickService-1} -> {ServiceClientCallPlace-pickService-1} +tr {ServiceClientCallTransition-placeService-0} {ServiceClientCallConnectPlace-placeService-0} -> {ServiceClientCallPlace-placeService-0} +tr {ServiceClientCallTransition-placeService-1} {ServiceClientCallConnectPlace-placeService-1} -> {ServiceClientCallPlace-placeService-1} +tr {ServiceClientCallTransition-sensorService-0} {ServiceClientCallConnectPlace-sensorService-0} -> {ServiceClientCallPlace-sensorService-0} +tr {ServiceClientRespConnectTransition-pickService-0} {ServiceClientRespConnectPlace-pickService-0} -> {L-ObjectPicked} {ServiceTogglePlace-pickService-0} +tr {ServiceClientRespConnectTransition-pickService-1} {ServiceClientRespConnectPlace-pickService-1} -> {R-ObjectPicked} {ServiceTogglePlace-pickService-1} +tr {ServiceClientRespConnectTransition-placeService-0} {ServiceClientRespConnectPlace-placeService-0} -> {L-ObjectPlaced} {ServiceTogglePlace-placeService-0} +tr {ServiceClientRespConnectTransition-placeService-1} {ServiceClientRespConnectPlace-placeService-1} -> {R-ObjectPlaced} {ServiceTogglePlace-placeService-1} +tr {ServiceClientRespConnectTransition-sensorService-0} {ServiceClientRespConnectPlace-sensorService-0} -> SensorResponse {ServiceTogglePlace-sensorService-0} +tr {ServiceClientRespTransition-pickService-0} {ServiceClientRespPlace-pickService-0} -> {ServiceClientRespConnectPlace-pickService-0} +tr {ServiceClientRespTransition-pickService-1} {ServiceClientRespPlace-pickService-1} -> {ServiceClientRespConnectPlace-pickService-1} +tr {ServiceClientRespTransition-placeService-0} {ServiceClientRespPlace-placeService-0} -> {ServiceClientRespConnectPlace-placeService-0} +tr {ServiceClientRespTransition-placeService-1} {ServiceClientRespPlace-placeService-1} -> {ServiceClientRespConnectPlace-placeService-1} +tr {ServiceClientRespTransition-sensorService-0} {ServiceClientRespPlace-sensorService-0} -> {ServiceClientRespConnectPlace-sensorService-0} +tr ShowFeedback FeedbackIn -> FeedbackDone +tr SortBlue {PD-0-SortBlue} ObjectPoolBlue -> BlueOut {PD-0-SortBlue} +tr SortGreen {PD-0-SortGreen} ObjectPoolGreen -> GreenOut {PD-0-SortGreen} +tr SortRed {PD-0-SortRed} ObjectPoolRed -> {PD-0-SortRed} RedOut +tr TransitionSafe SensorResponse -> Safe +tr TransitionUnsafe SensorResponse -> Unsafe +tr UnsafeToSensorCall Unsafe -> SensorCall +pl {CallbackCapacityPlace-LeftCellTopic-0-0} (10) +pl {CallbackCapacityPlace-RightCellTopic-0-0} (10) +pl {CallbackCapacityPlace-UITopic-0-0} (10) +pl {DispatcherCapacityPlace-LeftCellTopic-0} (16) +pl {DispatcherCapacityPlace-RightCellTopic-0} (16) +pl {DispatcherCapacityPlace-UITopic-0} (16) +pl {InputSignalFalsePlace-Blue} (1) +pl {InputSignalFalsePlace-Green} (1) +pl {InputSignalFalsePlace-PickFail} (1) +pl {InputSignalFalsePlace-PickSuccess} (1) +pl {InputSignalFalsePlace-PlaceFail} (1) +pl {InputSignalFalsePlace-PlaceSuccess} (1) +pl {InputSignalFalsePlace-Red} (1) +pl {InputSignalFalsePlace-Sensor} (1) +pl {InputSignalFalsePlace-Stop} (1) +pl ObjectPoolBlue (1) +pl ObjectPoolGreen (1) +pl ObjectPoolRed (1) +pl {PublisherCapacityPlace-LeftCellTopic-0} (10) +pl {PublisherCapacityPlace-LeftCellTopic-1} (10) +pl {PublisherCapacityPlace-RightCellTopic-0} (10) +pl {PublisherCapacityPlace-UITopic-0} (10) +pl {PublisherCapacityPlace-UITopic-1} (10) +pl {ServiceCallMultiInactivePlace-pickService-0} (1) +pl {ServiceCallMultiInactivePlace-pickService-1} (1) +pl {ServiceCallMultiInactivePlace-placeService-0} (1) +pl {ServiceCallMultiInactivePlace-placeService-1} (1) +pl {ServiceCallMultiInactivePlace-sensorService-0} (1) +pl {ServiceTogglePlace-pickService-0} (1) +pl {ServiceTogglePlace-pickService-1} (1) +pl {ServiceTogglePlace-placeService-0} (1) +pl {ServiceTogglePlace-placeService-1} (1) +pl {ServiceTogglePlace-sensorService-0} (1) +pl Unsafe (1) diff --git a/models/task-2/model-without-sync.pnml b/models/task-2/model-without-sync.pnml index 2a84101..779e16b 100644 --- a/models/task-2/model-without-sync.pnml +++ b/models/task-2/model-without-sync.pnml @@ -303,6 +303,39 @@ <text>L-Done</text> </name> </place> + + <transition id="L-ReqControl-T"> + <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> + <node>LeftController</node> + <subnet>LC1</subnet> + <type>discreteTransitionType</type> + <inputsignalclause></inputsignalclause> + </toolspecific> + <name> + <text>L-ReqControl-T</text> + </name> + </transition> + + <transition id="L-EndControl-T"> + <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> + <node>LeftController</node> + <subnet>LC1</subnet> + <type>discreteTransitionType</type> + <inputsignalclause></inputsignalclause> + </toolspecific> + <name> + <text>L-EndControl-T</text> + </name> + </transition> + + <arc id="la1" source="L-AwaitingControl" target="L-ReqControl-T"> + </arc> + <arc id="la2" source="L-ReqControl-T" target="L-Ready"> + </arc> + <arc id="la3" source="L-ObjectPlaced" target="L-EndControl-T"> + </arc> + <arc id="la4" source="L-EndControl-T" target="L-Done"> + </arc> </page> <page id="RightControllerPage"> @@ -355,6 +388,39 @@ <text>R-Done</text> </name> </place> + + <transition id="R-ReqControl-T"> + <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> + <node>RightController</node> + <subnet>RC1</subnet> + <type>discreteTransitionType</type> + <inputsignalclause></inputsignalclause> + </toolspecific> + <name> + <text>R-ReqControl-T</text> + </name> + </transition> + + <transition id="R-EndControl-T"> + <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> + <node>RightController</node> + <subnet>RC1</subnet> + <type>discreteTransitionType</type> + <inputsignalclause></inputsignalclause> + </toolspecific> + <name> + <text>R-EndControl-T</text> + </name> + </transition> + + <arc id="ra1" source="R-AwaitingControl" target="R-ReqControl-T"> + </arc> + <arc id="ra2" source="R-ReqControl-T" target="R-Ready"> + </arc> + <arc id="ra3" source="R-ObjectPlaced" target="R-EndControl-T"> + </arc> + <arc id="ra4" source="R-EndControl-T" target="R-Done"> + </arc> </page> <page id="FeedbackPage"> @@ -399,184 +465,6 @@ </arc> </page> - <page id="SynchronizerPage"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <type>nodePage</type> - </toolspecific> - <page id="GetControlService"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <type>serverPrototype</type> - <serviceName>getControlService</serviceName> - </toolspecific> - - <place id="GetControlIn"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>Synchronizer</node> - <subnet>GetControl</subnet> - </toolspecific> - <name> - <text>GetControlIn</text> - </name> - </place> - <place id="GetControlOut"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>Synchronizer</node> - <subnet>GetControl</subnet> - </toolspecific> - <name> - <text>GetControlOut</text> - </name> - </place> - <referencePlace id="GetSharedRef" ref="GetShared"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>Synchronizer</node> - <subnet>GetControl</subnet> - </toolspecific> - <name> - <text>GetSharedRef</text> - </name> - </referencePlace> - <transition id="Get"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>Synchronizer</node> - <subnet>GetControl</subnet> - <type>discreteTransitionType</type> - <inputsignalclause></inputsignalclause> - </toolspecific> - <name> - <text>Get</text> - </name> - </transition> - <arc id="a9" source="GetControlIn" target="Get"> - </arc> - <arc id="a10" source="Get" target="GetControlOut"> - </arc> - <arc id="a11" source="GetSharedRef" target="Get"> - </arc> - </page> - <page id="EndControlService"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <type>serverPrototype</type> - <serviceName>endControlService</serviceName> - </toolspecific> - - <place id="EndControlIn"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>Synchronizer</node> - <subnet>EndControl</subnet> - </toolspecific> - <name> - <text>EndControlIn</text> - </name> - </place> - <place id="EndControlOut"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>Synchronizer</node> - <subnet>EndControl</subnet> - </toolspecific> - <name> - <text>EndControlOut</text> - </name> - </place> - <referencePlace id="GetEndSharedRef" ref="GetShared"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>Synchronizer</node> - <subnet>EndControl</subnet> - </toolspecific> - <name> - <text>GetEndSharedRef</text> - </name> - </referencePlace> - <transition id="End"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>Synchronizer</node> - <subnet>EndControl</subnet> - <type>discreteTransitionType</type> - <inputsignalclause></inputsignalclause> - </toolspecific> - <name> - <text>End</text> - </name> - </transition> - <arc id="a12" source="EndControlIn" target="End"> - </arc> - <arc id="a13" source="End" target="EndControlOut"> - </arc> - <arc id="a13b" source="End" target="GetEndSharedRef"> - </arc> - </page> - <page id="SharedSpacePage"> - <place id="GetShared"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <node>Synchronizer</node> - <subnet>SharedSync</subnet> - <balloonMarking> - <tokens> - <token>{ "color":"NONE","name":"NONE","pickSuccess":"false","placeSuccess":"false", - "humanDetected":"false","sensorData":"NONE","trace":"NONE", "locked" : "true" } - </token> - </tokens> - </balloonMarking> - </toolspecific> - <initialMarking> - <text>1</text> - </initialMarking> - <name> - <text>GetShared</text> - </name> - </place> - </page> - </page> - - <transition id="GetControlServiceCall"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <type>serviceTransitionType</type> - <serviceName>getControlService</serviceName> - <serverInput>GetControlIn</serverInput> - <serverOutput>GetControlOut</serverOutput> - <serverCapacity>2</serverCapacity> - <channels> - <channel> - <cid>c1</cid> - <request>L-AwaitingControl</request> - <response>L-Ready</response> - </channel> - <channel> - <cid>c2</cid> - <request>R-AwaitingControl</request> - <response>R-Ready</response> - </channel> - </channels> - </toolspecific> - <name> - <text>GetControlServiceCall</text> - </name> - </transition> - <transition id="EndControlServiceCall"> - <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> - <type>serviceTransitionType</type> - <serviceName>endControlService</serviceName> - <serverInput>EndControlIn</serverInput> - <serverOutput>EndControlOut</serverOutput> - <serverCapacity>2</serverCapacity> - <channels> - <channel> - <cid>c3</cid> - <request>L-ObjectPlaced</request> - <response>L-Done</response> - </channel> - <channel> - <cid>c4</cid> - <request>R-ObjectPlaced</request> - <response>R-Done</response> - </channel> - </channels> - </toolspecific> - <name> - <text>EndControlServiceCall</text> - </name> - </transition> - <transition id="PickServiceCall"> <toolspecific tool="de.tudresden.inf.st.pnml.distributedPN" version="0.1"> <type>serviceTransitionType</type> -- GitLab