material for first exercise, toolings for both exercises, docker for ROS1

docker/Dockerfile

+# Use the official Ubuntu 20.04 base image
+FROM ubuntu:20.04
+
+# Set environment variables to non-interactive to prevent prompts during installation
+ENV DEBIAN_FRONTEND=noninteractive
+
+# Update the package list and install required tools
+RUN apt-get update && apt-get install -y \
+    locales \
+    curl \
+    gnupg2 \
+    lsb-release \
+    && locale-gen en_US.UTF-8
+
+# Set locale
+ENV LANG=en_US.UTF-8
+ENV LC_ALL=en_US.UTF-8
+
+# Add the ROS repository
+RUN curl -sSL http://packages.ros.org/ros.key | apt-key add - && \
+    sh -c 'echo "deb http://packages.ros.org/ros/ubuntu $(lsb_release -sc) main" > /etc/apt/sources.list.d/ros-latest.list'
+
+# Update and install ROS Noetic
+RUN apt-get update && apt-get install -y \
+    ros-noetic-ros-base \
+    && apt-get clean
+
+# Initialize ROS environment
+RUN echo "source /opt/ros/noetic/setup.bash" >> ~/.bashrc
+
+# Install additional tools
+RUN apt-get update && apt-get install -y \
+    python3-rosdep \
+    python3-rosinstall \
+    python3-rosinstall-generator \
+    python3-wstool \
+    build-essential
+
+# Initialize rosdep
+RUN rosdep init && rosdep update
+
+# Create an entrypoint to source ROS and run roscore
+COPY entrypoint.sh /entrypoint.sh
+RUN chmod +x /entrypoint.sh
+
+# Expose ROS default ports
+EXPOSE 11311
+
+# Set the entrypoint
+ENTRYPOINT ["/entrypoint.sh"]

docker/entrypoint.sh

+#!/bin/bash
+# Source ROS setup
+source /opt/ros/noetic/setup.bash
+# Start roscore
+exec roscore

docker/manual.md

+Build: docker build -t ros-noetic .
+
+Run: docker run --rm -it --network=host ros-noetic

models/model-top-flatted-red.net

+# from 103 place(s), 86 transition(s), 277 arc(s)
+# R4  |- agglomerated 14 place(s)
+# .   |- removed 14 identity transition(s)
+# R4  |- agglomerated 2 place(s)
+# .   |- removed 2 identity transition(s)
+# R1b |- removed 4 redundant place(s)
+# R4l |- agglomerated 2 place(s)
+# .   |- removed 4 identity transition(s)
+# R1  |- removed 2 constant or duplicated place(s)
+# R4  |- agglomerated 2 place(s)
+# .   |- removed 2 identity transition(s)
+# R1b |- removed 1 redundant place(s)
+# R4l |- agglomerated 1 place(s)
+# .   |- removed 2 identity transition(s)
+# R1  |- removed 1 constant or duplicated place(s)
+# R4  |- agglomerated 1 place(s)
+# .   |- removed 1 identity transition(s)
+# R1b |- removed 1 redundant place(s)
+# left 72 place(s), 61 transition(s), 203 arc(s)
+# 0.014s
+
+# a-prefix = a
+
+# generated equations
+# A |- a1 = {DispatcherInputPlace-LeftCellTopic-0} + {ChannelConnectorPlace-LeftCellTopic}
+# A |- a2 = {DispatcherInputPlace-RightCellTopic-0} + {ChannelConnectorPlace-RightCellTopic}
+# A |- a3 = {DispatcherInputPlace-UITopic-0} + {ChannelConnectorPlace-UITopic}
+# A |- a4 = FeedbackDone + FeedbackIn
+# A |- a5 = {L-ObjectPlaced} + {L-ObjectPicked}
+# A |- a6 = {R-ObjectPlaced} + {R-ObjectPicked}
+# A |- a7 = {ServiceClientCallPlace-endControlService-0} + {ServiceClientCallConnectPlace-endControlService-0}
+# A |- a8 = {ServiceClientCallPlace-endControlService-1} + {ServiceClientCallConnectPlace-endControlService-1}
+# A |- a9 = {ServiceClientCallPlace-getControlService-0} + {ServiceClientCallConnectPlace-getControlService-0}
+# A |- a10 = {ServiceClientCallPlace-getControlService-1} + {ServiceClientCallConnectPlace-getControlService-1}
+# A |- a11 = {ServiceClientRespConnectPlace-endControlService-0} + {ServiceClientRespPlace-endControlService-0}
+# A |- a12 = {ServiceClientRespConnectPlace-endControlService-1} + {ServiceClientRespPlace-endControlService-1}
+# A |- a13 = {ServiceClientRespConnectPlace-getControlService-0} + {ServiceClientRespPlace-getControlService-0}
+# A |- a14 = {ServiceClientRespConnectPlace-getControlService-1} + {ServiceClientRespPlace-getControlService-1}
+# A |- a15 = a5 + {L-Ready}
+# A |- a16 = a6 + {R-Ready}
+# R |- {InputSignalTruePlace-Blue} = {PD-0-SortBlue}
+# R |- {InputSignalTruePlace-Green} = {PD-0-SortGreen}
+# R |- {ServiceCallMultiActivePlace-endControlService-0} = {EndControlIn-INSTANCE-0} + {EndControlOut-INSTANCE-0}
+# R |- {ServiceCallMultiActivePlace-getControlService-1} = {ServiceCallMultiFlagPlace-getControlService-1-0} + {ServiceCallMultiFlagPlace-getControlService-1-1}
+# A |- a17 = {InputSignalFalsePlace-Blue} + {PD-0-SortBlue}
+# A |- a18 = {InputSignalFalsePlace-Green} + {PD-0-SortGreen}
+# R |- a17 = 1
+# R |- a18 = 1
+# A |- a19 = BlueOut + ObjectPoolBlue
+# A |- a20 = GreenOut + ObjectPoolGreen
+# R |- {InputSignalTruePlace-Red} = {PD-0-SortRed}
+# A |- a21 = {InputSignalFalsePlace-Red} + {PD-0-SortRed}
+# R |- a21 = 1
+# A |- a22 = RedOut + ObjectPoolRed
+# R |- {ServiceCallMultiActivePlace-endControlService-1} = {EndControlIn-INSTANCE-1} + {EndControlOut-INSTANCE-1}
+
+net ModelTop
+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} a4 
+tr {CallbackOverflowTransition-LeftCellTopic-0-0} {CallbackConnectorPlace-LeftCellTopic-0-0}*10 {CallbackInputPlace-LeftCellTopic-0-0}  -> {CallbackConnectorPlace-LeftCellTopic-0-0}*10 
+tr {CallbackOverflowTransition-RightCellTopic-0-0} {CallbackConnectorPlace-RightCellTopic-0-0}*10 {CallbackInputPlace-RightCellTopic-0-0}  -> {CallbackConnectorPlace-RightCellTopic-0-0}*10 
+tr {CallbackOverflowTransition-UITopic-0-0} {CallbackConnectorPlace-UITopic-0-0}*10 {CallbackInputPlace-UITopic-0-0}  -> {CallbackConnectorPlace-UITopic-0-0}*10 
+tr {DispatcherInputTransition-LeftCellTopic-0} a1 {DispatcherCapacityPlace-LeftCellTopic-0}  -> {DispatcherConnectorPlace-LeftCellTopic-0} 
+tr {DispatcherInputTransition-RightCellTopic-0} a2 {DispatcherCapacityPlace-RightCellTopic-0}  -> {DispatcherConnectorPlace-RightCellTopic-0} 
+tr {DispatcherInputTransition-UITopic-0} a3 {DispatcherCapacityPlace-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} a1 {DispatcherConnectorPlace-LeftCellTopic-0}*16  -> {DispatcherConnectorPlace-LeftCellTopic-0}*16 
+tr {DispatcherOverflowTransition-RightCellTopic-0} a2 {DispatcherConnectorPlace-RightCellTopic-0}*16  -> {DispatcherConnectorPlace-RightCellTopic-0}*16 
+tr {DispatcherOverflowTransition-UITopic-0} a3 {DispatcherConnectorPlace-UITopic-0}*16  -> {DispatcherConnectorPlace-UITopic-0}*16 
+tr {End-INSTANCE-0} {EndControlIn-INSTANCE-0}  -> {EndControlOut-INSTANCE-0} GetShared 
+tr {End-INSTANCE-1} {EndControlIn-INSTANCE-1}  -> {EndControlOut-INSTANCE-1} GetShared 
+tr {Get-INSTANCE-0} {GetControlIn-INSTANCE-0} GetShared  -> {GetControlOut-INSTANCE-0} 
+tr {Get-INSTANCE-1} {GetControlIn-INSTANCE-1} GetShared  -> {GetControlOut-INSTANCE-1} 
+tr {PublisherInputTransition-LeftCellTopic-0} a22 {PublisherCapacityPlace-LeftCellTopic-0}  -> {PublisherConnectorPlace-LeftCellTopic-0} 
+tr {PublisherInputTransition-LeftCellTopic-1} a19 {PublisherCapacityPlace-LeftCellTopic-1}  -> {PublisherConnectorPlace-LeftCellTopic-1} 
+tr {PublisherInputTransition-RightCellTopic-0} a20 {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}  -> a1 {PublisherCapacityPlace-LeftCellTopic-0} 
+tr {PublisherOutputTransition-LeftCellTopic-1} {PublisherConnectorPlace-LeftCellTopic-1}  -> a1 {PublisherCapacityPlace-LeftCellTopic-1} 
+tr {PublisherOutputTransition-RightCellTopic-0} {PublisherConnectorPlace-RightCellTopic-0}  -> a2 {PublisherCapacityPlace-RightCellTopic-0} 
+tr {PublisherOutputTransition-UITopic-0} {PublisherConnectorPlace-UITopic-0}  -> a3 {PublisherCapacityPlace-UITopic-0} 
+tr {PublisherOutputTransition-UITopic-1} {PublisherConnectorPlace-UITopic-1}  -> a3 {PublisherCapacityPlace-UITopic-1} 
+tr {PublisherOverflowTransition-LeftCellTopic-0} a22 {PublisherConnectorPlace-LeftCellTopic-0}*10  -> {PublisherConnectorPlace-LeftCellTopic-0}*10 
+tr {PublisherOverflowTransition-LeftCellTopic-1} a19 {PublisherConnectorPlace-LeftCellTopic-1}*10  -> {PublisherConnectorPlace-LeftCellTopic-1}*10 
+tr {PublisherOverflowTransition-RightCellTopic-0} a20 {PublisherConnectorPlace-RightCellTopic-0}*10  -> {PublisherConnectorPlace-RightCellTopic-0}*10 
+tr {PublisherOverflowTransition-UITopic-0} {L-Done} {PublisherConnectorPlace-UITopic-0}*10  -> {PublisherConnectorPlace-UITopic-0}*10 
+tr {PublisherOverflowTransition-UITopic-1} {PublisherConnectorPlace-UITopic-1}*10 {R-Done}  -> {PublisherConnectorPlace-UITopic-1}*10 
+tr {ServiceCallMultiEntryTransition-endControlService-0-0} {ServiceCallMultiInactivePlace-endControlService-0} a7  -> {EndControlIn-INSTANCE-0} {ServiceCallMultiFlagPlace-endControlService-0-0} 
+tr {ServiceCallMultiEntryTransition-endControlService-0-1} {ServiceCallMultiInactivePlace-endControlService-0} a8  -> {EndControlIn-INSTANCE-0} {ServiceCallMultiFlagPlace-endControlService-0-1} 
+tr {ServiceCallMultiEntryTransition-endControlService-1-0} {ServiceCallMultiInactivePlace-endControlService-1} a7  -> {EndControlIn-INSTANCE-1} {ServiceCallMultiFlagPlace-endControlService-1-0} 
+tr {ServiceCallMultiEntryTransition-endControlService-1-1} {ServiceCallMultiInactivePlace-endControlService-1} a8  -> {EndControlIn-INSTANCE-1} {ServiceCallMultiFlagPlace-endControlService-1-1} 
+tr {ServiceCallMultiEntryTransition-getControlService-0-0} {ServiceCallMultiInactivePlace-getControlService-0} a9  -> {GetControlIn-INSTANCE-0} {ServiceCallMultiActivePlace-getControlService-0} {ServiceCallMultiFlagPlace-getControlService-0-0} 
+tr {ServiceCallMultiEntryTransition-getControlService-0-1} {ServiceCallMultiInactivePlace-getControlService-0} a10  -> {GetControlIn-INSTANCE-0} {ServiceCallMultiActivePlace-getControlService-0} {ServiceCallMultiFlagPlace-getControlService-0-1} 
+tr {ServiceCallMultiEntryTransition-getControlService-1-0} {ServiceCallMultiInactivePlace-getControlService-1} a9  -> {GetControlIn-INSTANCE-1} {ServiceCallMultiFlagPlace-getControlService-1-0} 
+tr {ServiceCallMultiEntryTransition-getControlService-1-1} {ServiceCallMultiInactivePlace-getControlService-1} a10  -> {GetControlIn-INSTANCE-1} {ServiceCallMultiFlagPlace-getControlService-1-1} 
+tr {ServiceCallMultiExitTransition-endControlService-0-0} {EndControlOut-INSTANCE-0} {ServiceCallMultiFlagPlace-endControlService-0-0}  -> {ServiceCallMultiInactivePlace-endControlService-0} a11 
+tr {ServiceCallMultiExitTransition-endControlService-0-1} {EndControlOut-INSTANCE-0} {ServiceCallMultiFlagPlace-endControlService-0-1}  -> {ServiceCallMultiInactivePlace-endControlService-0} a12 
+tr {ServiceCallMultiExitTransition-endControlService-1-0} {EndControlOut-INSTANCE-1} {ServiceCallMultiFlagPlace-endControlService-1-0}  -> {ServiceCallMultiInactivePlace-endControlService-1} a11 
+tr {ServiceCallMultiExitTransition-endControlService-1-1} {EndControlOut-INSTANCE-1} {ServiceCallMultiFlagPlace-endControlService-1-1}  -> {ServiceCallMultiInactivePlace-endControlService-1} a12 
+tr {ServiceCallMultiExitTransition-getControlService-0-0} {GetControlOut-INSTANCE-0} {ServiceCallMultiActivePlace-getControlService-0} {ServiceCallMultiFlagPlace-getControlService-0-0}  -> {ServiceCallMultiInactivePlace-getControlService-0} a13 
+tr {ServiceCallMultiExitTransition-getControlService-0-1} {GetControlOut-INSTANCE-0} {ServiceCallMultiActivePlace-getControlService-0} {ServiceCallMultiFlagPlace-getControlService-0-1}  -> {ServiceCallMultiInactivePlace-getControlService-0} a14 
+tr {ServiceCallMultiExitTransition-getControlService-1-0} {GetControlOut-INSTANCE-1} {ServiceCallMultiFlagPlace-getControlService-1-0}  -> {ServiceCallMultiInactivePlace-getControlService-1} a13 
+tr {ServiceCallMultiExitTransition-getControlService-1-1} {GetControlOut-INSTANCE-1} {ServiceCallMultiFlagPlace-getControlService-1-1}  -> {ServiceCallMultiInactivePlace-getControlService-1} a14 
+tr {ServiceClientCallConnectTransition-endControlService-0} a15 {ServiceTogglePlace-endControlService-0}  -> a7 
+tr {ServiceClientCallConnectTransition-endControlService-1} a16 {ServiceTogglePlace-endControlService-1}  -> a8 
+tr {ServiceClientCallConnectTransition-getControlService-0} {L-AwaitingControl} {ServiceTogglePlace-getControlService-0}  -> a9 
+tr {ServiceClientCallConnectTransition-getControlService-1} {R-AwaitingControl} {ServiceTogglePlace-getControlService-1}  -> a10 
+tr {ServiceClientRespConnectTransition-endControlService-0} a11  -> {L-Done} {ServiceTogglePlace-endControlService-0} 
+tr {ServiceClientRespConnectTransition-endControlService-1} a12  -> {R-Done} {ServiceTogglePlace-endControlService-1} 
+tr {ServiceClientRespConnectTransition-getControlService-0} a13  -> a15 {ServiceTogglePlace-getControlService-0} 
+tr {ServiceClientRespConnectTransition-getControlService-1} a14  -> a16 {ServiceTogglePlace-getControlService-1} 
+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 GetShared (1)
+pl a19 (1)
+pl a20 (1)
+pl a22 (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-endControlService-0} (1)
+pl {ServiceCallMultiInactivePlace-endControlService-1} (1)
+pl {ServiceCallMultiInactivePlace-getControlService-0} (1)
+pl {ServiceCallMultiInactivePlace-getControlService-1} (1)
+pl {ServiceTogglePlace-endControlService-0} (1)
+pl {ServiceTogglePlace-endControlService-1} (1)
+pl {ServiceTogglePlace-getControlService-0} (1)
+pl {ServiceTogglePlace-getControlService-1} (1)

models/model-top-no-inh.net

+net ModelTop
+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} {CallbackConnectorPlace-LeftCellTopic-0-0}*10 {CallbackInputPlace-LeftCellTopic-0-0} -> {CallbackConnectorPlace-LeftCellTopic-0-0}*10 
+tr {CallbackOverflowTransition-RightCellTopic-0-0} {CallbackConnectorPlace-RightCellTopic-0-0}*10 {CallbackInputPlace-RightCellTopic-0-0} -> {CallbackConnectorPlace-RightCellTopic-0-0}*10 
+tr {CallbackOverflowTransition-UITopic-0-0} {CallbackConnectorPlace-UITopic-0-0}*10 {CallbackInputPlace-UITopic-0-0} -> {CallbackConnectorPlace-UITopic-0-0}*10 
+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} {DispatcherConnectorPlace-LeftCellTopic-0}*16 {DispatcherInputPlace-LeftCellTopic-0} -> {DispatcherConnectorPlace-LeftCellTopic-0}*16 
+tr {DispatcherOverflowTransition-RightCellTopic-0} {DispatcherConnectorPlace-RightCellTopic-0}*16 {DispatcherInputPlace-RightCellTopic-0} -> {DispatcherConnectorPlace-RightCellTopic-0}*16 
+tr {DispatcherOverflowTransition-UITopic-0} {DispatcherConnectorPlace-UITopic-0}*16 {DispatcherInputPlace-UITopic-0} -> {DispatcherConnectorPlace-UITopic-0}*16 
+tr {End-INSTANCE-0} {EndControlIn-INSTANCE-0} -> {EndControlOut-INSTANCE-0} GetShared 
+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 {InputSignalToFalseTransition-Blue} {PD-0-SortBlue} {InputSignalTruePlace-Blue} -> {InputSignalFalsePlace-Blue} 
+tr {InputSignalToFalseTransition-Green} {InputSignalTruePlace-Green} {PD-0-SortGreen} -> {InputSignalFalsePlace-Green} 
+tr {InputSignalToFalseTransition-Red} {InputSignalTruePlace-Red} {PD-0-SortRed} -> {InputSignalFalsePlace-Red} 
+tr {InputSignalToTrueTransition-Blue} {InputSignalFalsePlace-Blue} -> {PD-0-SortBlue} {InputSignalTruePlace-Blue} 
+tr {InputSignalToTrueTransition-Green} {InputSignalFalsePlace-Green} -> {InputSignalTruePlace-Green} {PD-0-SortGreen} 
+tr {InputSignalToTrueTransition-Red} {InputSignalFalsePlace-Red} -> {InputSignalTruePlace-Red} {PD-0-SortRed} 
+tr {L-Pick} {L-Ready} -> {L-ObjectPicked} 
+tr {L-Place} {L-ObjectPicked} -> {L-ObjectPlaced} 
+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} {PublisherConnectorPlace-LeftCellTopic-0}*10 RedOut -> {PublisherConnectorPlace-LeftCellTopic-0}*10 
+tr {PublisherOverflowTransition-LeftCellTopic-1} BlueOut {PublisherConnectorPlace-LeftCellTopic-1}*10 -> {PublisherConnectorPlace-LeftCellTopic-1}*10 
+tr {PublisherOverflowTransition-RightCellTopic-0} GreenOut {PublisherConnectorPlace-RightCellTopic-0}*10 -> {PublisherConnectorPlace-RightCellTopic-0}*10 
+tr {PublisherOverflowTransition-UITopic-0} {L-Done} {PublisherConnectorPlace-UITopic-0}*10 -> {PublisherConnectorPlace-UITopic-0}*10 
+tr {PublisherOverflowTransition-UITopic-1} {PublisherConnectorPlace-UITopic-1}*10 {R-Done} -> {PublisherConnectorPlace-UITopic-1}*10 
+tr {R-Pick} {R-Ready} -> {R-ObjectPicked} 
+tr {R-Place} {R-ObjectPicked} -> {R-ObjectPlaced} 
+tr {ServiceCallMultiEntryTransition-endControlService-0-0} {ServiceClientCallPlace-endControlService-0} {ServiceCallMultiInactivePlace-endControlService-0} -> {EndControlIn-INSTANCE-0} {ServiceCallMultiActivePlace-endControlService-0} {ServiceCallMultiFlagPlace-endControlService-0-0} 
+tr {ServiceCallMultiEntryTransition-endControlService-0-1} {ServiceCallMultiInactivePlace-endControlService-0} {ServiceClientCallPlace-endControlService-1} -> {EndControlIn-INSTANCE-0} {ServiceCallMultiActivePlace-endControlService-0} {ServiceCallMultiFlagPlace-endControlService-0-1} 
+tr {ServiceCallMultiEntryTransition-endControlService-1-0} {ServiceClientCallPlace-endControlService-0} {ServiceCallMultiInactivePlace-endControlService-1} -> {EndControlIn-INSTANCE-1} {ServiceCallMultiActivePlace-endControlService-1} {ServiceCallMultiFlagPlace-endControlService-1-0} 
+tr {ServiceCallMultiEntryTransition-endControlService-1-1} {ServiceClientCallPlace-endControlService-1} {ServiceCallMultiInactivePlace-endControlService-1} -> {EndControlIn-INSTANCE-1} {ServiceCallMultiActivePlace-endControlService-1} {ServiceCallMultiFlagPlace-endControlService-1-1} 
+tr {ServiceCallMultiEntryTransition-getControlService-0-0} {ServiceClientCallPlace-getControlService-0} {ServiceCallMultiInactivePlace-getControlService-0} -> {GetControlIn-INSTANCE-0} {ServiceCallMultiActivePlace-getControlService-0} {ServiceCallMultiFlagPlace-getControlService-0-0} 
+tr {ServiceCallMultiEntryTransition-getControlService-0-1} {ServiceCallMultiInactivePlace-getControlService-0} {ServiceClientCallPlace-getControlService-1} -> {GetControlIn-INSTANCE-0} {ServiceCallMultiActivePlace-getControlService-0} {ServiceCallMultiFlagPlace-getControlService-0-1} 
+tr {ServiceCallMultiEntryTransition-getControlService-1-0} {ServiceClientCallPlace-getControlService-0} {ServiceCallMultiInactivePlace-getControlService-1} -> {GetControlIn-INSTANCE-1} {ServiceCallMultiActivePlace-getControlService-1} {ServiceCallMultiFlagPlace-getControlService-1-0} 
+tr {ServiceCallMultiEntryTransition-getControlService-1-1} {ServiceClientCallPlace-getControlService-1} {ServiceCallMultiInactivePlace-getControlService-1} -> {GetControlIn-INSTANCE-1} {ServiceCallMultiActivePlace-getControlService-1} {ServiceCallMultiFlagPlace-getControlService-1-1} 
+tr {ServiceCallMultiExitTransition-endControlService-0-0} {EndControlOut-INSTANCE-0} {ServiceCallMultiActivePlace-endControlService-0} {ServiceCallMultiFlagPlace-endControlService-0-0} -> {ServiceCallMultiInactivePlace-endControlService-0} {ServiceClientRespPlace-endControlService-0} 
+tr {ServiceCallMultiExitTransition-endControlService-0-1} {EndControlOut-INSTANCE-0} {ServiceCallMultiActivePlace-endControlService-0} {ServiceCallMultiFlagPlace-endControlService-0-1} -> {ServiceCallMultiInactivePlace-endControlService-0} {ServiceClientRespPlace-endControlService-1} 
+tr {ServiceCallMultiExitTransition-endControlService-1-0} {EndControlOut-INSTANCE-1} {ServiceCallMultiActivePlace-endControlService-1} {ServiceCallMultiFlagPlace-endControlService-1-0} -> {ServiceCallMultiInactivePlace-endControlService-1} {ServiceClientRespPlace-endControlService-0} 
+tr {ServiceCallMultiExitTransition-endControlService-1-1} {EndControlOut-INSTANCE-1} {ServiceCallMultiActivePlace-endControlService-1} {ServiceCallMultiFlagPlace-endControlService-1-1} -> {ServiceCallMultiInactivePlace-endControlService-1} {ServiceClientRespPlace-endControlService-1} 
+tr {ServiceCallMultiExitTransition-getControlService-0-0} {GetControlOut-INSTANCE-0} {ServiceCallMultiActivePlace-getControlService-0} {ServiceCallMultiFlagPlace-getControlService-0-0} -> {ServiceCallMultiInactivePlace-getControlService-0} {ServiceClientRespPlace-getControlService-0} 
+tr {ServiceCallMultiExitTransition-getControlService-0-1} {GetControlOut-INSTANCE-0} {ServiceCallMultiActivePlace-getControlService-0} {ServiceCallMultiFlagPlace-getControlService-0-1} -> {ServiceCallMultiInactivePlace-getControlService-0} {ServiceClientRespPlace-getControlService-1} 
+tr {ServiceCallMultiExitTransition-getControlService-1-0} {GetControlOut-INSTANCE-1} {ServiceCallMultiActivePlace-getControlService-1} {ServiceCallMultiFlagPlace-getControlService-1-0} -> {ServiceCallMultiInactivePlace-getControlService-1} {ServiceClientRespPlace-getControlService-0} 
+tr {ServiceCallMultiExitTransition-getControlService-1-1} {GetControlOut-INSTANCE-1} {ServiceCallMultiActivePlace-getControlService-1} {ServiceCallMultiFlagPlace-getControlService-1-1} -> {ServiceCallMultiInactivePlace-getControlService-1} {ServiceClientRespPlace-getControlService-1} 
+tr {ServiceClientCallConnectTransition-endControlService-0} {L-ObjectPlaced} {ServiceTogglePlace-endControlService-0} -> {ServiceClientCallConnectPlace-endControlService-0} 
+tr {ServiceClientCallConnectTransition-endControlService-1} {R-ObjectPlaced} {ServiceTogglePlace-endControlService-1} -> {ServiceClientCallConnectPlace-endControlService-1} 
+tr {ServiceClientCallConnectTransition-getControlService-0} {L-AwaitingControl} {ServiceTogglePlace-getControlService-0} -> {ServiceClientCallConnectPlace-getControlService-0} 
+tr {ServiceClientCallConnectTransition-getControlService-1} {R-AwaitingControl} {ServiceTogglePlace-getControlService-1} -> {ServiceClientCallConnectPlace-getControlService-1} 
+tr {ServiceClientCallTransition-endControlService-0} {ServiceClientCallConnectPlace-endControlService-0} -> {ServiceClientCallPlace-endControlService-0} 
+tr {ServiceClientCallTransition-endControlService-1} {ServiceClientCallConnectPlace-endControlService-1} -> {ServiceClientCallPlace-endControlService-1} 
+tr {ServiceClientCallTransition-getControlService-0} {ServiceClientCallConnectPlace-getControlService-0} -> {ServiceClientCallPlace-getControlService-0} 
+tr {ServiceClientCallTransition-getControlService-1} {ServiceClientCallConnectPlace-getControlService-1} -> {ServiceClientCallPlace-getControlService-1} 
+tr {ServiceClientRespConnectTransition-endControlService-0} {ServiceClientRespConnectPlace-endControlService-0} -> {L-Done} {ServiceTogglePlace-endControlService-0} 
+tr {ServiceClientRespConnectTransition-endControlService-1} {ServiceClientRespConnectPlace-endControlService-1} -> {R-Done} {ServiceTogglePlace-endControlService-1} 
+tr {ServiceClientRespConnectTransition-getControlService-0} {ServiceClientRespConnectPlace-getControlService-0} -> {L-Ready} {ServiceTogglePlace-getControlService-0} 
+tr {ServiceClientRespConnectTransition-getControlService-1} {ServiceClientRespConnectPlace-getControlService-1} -> {R-Ready} {ServiceTogglePlace-getControlService-1} 
+tr {ServiceClientRespTransition-endControlService-0} {ServiceClientRespPlace-endControlService-0} -> {ServiceClientRespConnectPlace-endControlService-0} 
+tr {ServiceClientRespTransition-endControlService-1} {ServiceClientRespPlace-endControlService-1} -> {ServiceClientRespConnectPlace-endControlService-1} 
+tr {ServiceClientRespTransition-getControlService-0} {ServiceClientRespPlace-getControlService-0} -> {ServiceClientRespConnectPlace-getControlService-0} 
+tr {ServiceClientRespTransition-getControlService-1} {ServiceClientRespPlace-getControlService-1} -> {ServiceClientRespConnectPlace-getControlService-1} 
+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 
+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 GetShared (1)
+pl {InputSignalFalsePlace-Blue} (1)
+pl {InputSignalFalsePlace-Green} (1)
+pl {InputSignalFalsePlace-Red} (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-endControlService-0} (1)
+pl {ServiceCallMultiInactivePlace-endControlService-1} (1)
+pl {ServiceCallMultiInactivePlace-getControlService-0} (1)
+pl {ServiceCallMultiInactivePlace-getControlService-1} (1)
+pl {ServiceTogglePlace-endControlService-0} (1)
+pl {ServiceTogglePlace-endControlService-1} (1)
+pl {ServiceTogglePlace-getControlService-0} (1)
+pl {ServiceTogglePlace-getControlService-1} (1)

models/task-2/model-without-sync-flatted.net

-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)

tools/tina-3.7.0/CHANGES

+Changes from 3.0.0 to current:
+-----------------------------
+
+Now summarized on http://www.laas.fr/tina/news.php
+
+
+Changes from 2.10.0 to 3.0.0:
+-----------------------------
+
+In addition to  bug fixes and many improvements  of 2.10.0 tools, Tina
+version 3.0.0 introduces five new tools:
+
+frac -- support  for high-level descriptions in Fiacre:  As of version
+2.9.0, tina supports an extension of Time Petri Nets with data actions
+and  preconditions specified  in C  (see  the description  of the  tts
+format in manual pages).  A higher level notation is now available, in
+a language called Fiacre.  Fiacre  descriptions can be compiled to tts
+descriptions  accepted by  tina by  a dedicated  compiler,  Frac.  The
+Fiacre language and the Frac compiler are described and made available
+in a companion site (http://www.laas.fr/fiacre).
+
+sift: it is a specialization of  the tina tool, it offers less options
+than tina  but implements them  more efficiently; sift is  faster than
+tina and  makes use  of considerably less  space. sift also  allows to
+check reachability properties on the fly.
+
+pathto: a utility  program; given a kripke transition  system in a ktz
+file and  a target state,  pathto computes and  prints a path  to that
+state. pathto  is mostly useful for for  building transition sequences
+leading to counter-example states computed by sift.
+
+play: allows to  simulate net descriptions in all  formats accepted by
+tina.   Its capabilities  are  similar  to those  provided  by the  nd
+stepper except that play may also simulate .tts descriptions.
+
+muse:  (in progress) a  modal mu-calculus  model checker  operating on
+kripke transition systems represented in .ktz format.
+
+Check the  Fiacre pages and the  manual pages in  directories doc/* of
+the distributions for usage details.
+
+
+Changes from 2.9.0 to 2.10.0:
+-----------------------------
+
+The standard tina distribution  now supports the "Stopwatch Time Petri
+nets", formerly  in a specific distribution, introduced in paper:
+
+  B. Berthomieu, D. Lime, O. H. Roux, F. Vernadat,
+  Reachability Problems and Abstract State Spaces for Time Petri Nets
+  with Stopwatches,
+  Journal of Discrete Event Dynamic Systems 17:133-158, 2007.
+
+
+Changes following the support of stopwatches:
+
+- The graphic  editor and  all net formats  support two more  types of
+arc: stopwatch arcs and stopwatch-inhibitor arcs.  These arcs serve to
+stop/resume the clock of their target transition.
+
+- In the  textual .net format, stopwatch  and stopwatch-inhibitor arcs
+are  specified  like  read  and  inhibitor  arcs,  respectively,  just
+replacing symbol "?" by "!", as in e.g.:
+
+            tr t0 [4,5] p1 p2!1 -> p3*3
+            tr t1 [3,w[ p6 p5!-3 -> p8 
+
+The tool tina has two extra flags:
+
+- flag  -grid  n/d specifies  a  grid  size  for overapproximation  of
+temporal domains (default none) in presence of stopwatches.
+
+- flag  -pk   (1|2|3)  specifies  the  format   of  inequality  system
+coefficients   and  constants   in  state   classes  in   presence  of
+stopwatches: 1 means 32 bit (fast but high risks of overflow), 2 means
+64  bits (default),  3  means arbitrary  precision  integers (may  not
+overflow, but computationally expensive).
+
+Support  of  stopwatches   currently  suffers  some  restrictions.  In
+particular:
+
+- Some constructions are not implemented  for SwTPN's yet; tina modes
+  -D/-F/-U/-A are not supported;
+
+- Unbounded static intervals are not supported for SwTPNs in mode -S;
+
+- The  plan tool does not support stopwatch arcs yet,  so the  counter
+  examples computed by the model checker cannot be timed (nor reloaded
+  into the nd stepper if using selt from nd);
+
+Finally, it  should be stressed  than computation of state  classes of
+SwTPN's is not  guaranteed to terminate in general,  unless the net is
+intrinsically bounded  AND some grid  size is specified by  flag -grid
+(check the above papers for details). Also, computing state classes in
+presence of stopwatches can be very slow and space consuming.
+
+
+The other changes include:
+
+- nd:  The nd  editor  now  provides a  toolbar.   The former  graphic
+bindings are still supported (when toolbar is in selection mode).  The
+graphic bindings  have been cleaned  up, specially on MacOS;  they are
+recalled  in the  nd  window on  startup.   Check nd->preferences  for
+options;
+
+- tools:   besides  bug   fixes  and   many  optimizations,   flag  -s
+(boundedness test) of tina now has  two options only: -s 0 removes any
+boundedness  check, -s 1  (default) checks  a necessary  condition for
+unboundedness of the underlying petri net (omitting time constraints).
+-s 1  is cheap but with  a small risk  of non termination; for  a true
+boundedness  check on  untimed  nets,  one should  use  the costly  -C
+option (on untimed nets).
+
+- the pnml parser now handles pages (one page actually);
+
+
+Changes from 2.8.4 to 2.9.0:
+-----------------------------
+
+Besides  many   improvements,  it  introduces   static  priorities:  A
+transition is  firable at  some instant if  no transition  with higher
+priority is  firable at the  same instant.  In absence  of priorities,
+2.9.0  behaves  exactly  like  2.8.4  (in  spite  of  minor  ergonomic
+differences) and is fully upward-compatible.
+
+- Priorities  may be  specified graphically,  by drawing  arcs between
+transitions, from  that with higher  priority, or textually  with "pr"
+declarations  (check doc/formats/net.txt  for details).   The priority
+relation is the transitive closure  of the specified relation, it must
+be irreflexive.  All tools  support priorities, but priorities are not
+meaningfull in  all state space abstractions  (notably in coverability
+graphs (-C)  and state classes (-W)).  The  adequate constructions for
+handling priorities are the reachability graph (mode -R) in absence of
+time constraints and the strong state class graph (or zone graph, mode
+-S) with time constraints.  More constructions will support priorities
+in  the  future  (including  covering  state graphs  (mode  -V)).   By
+default, the state space  abstraction tool selects a construction that
+handles all features present in the net.
+
+- The nd  editor and other  tools have been  improved in an  number of
+ways  favoring robustness, ease  of use  and performances.
+
+
+Changes from 2.8.0 to 2.8.4:
+-----------------------------
+
+Besides bug fixes and many  small improvements, the changes from 2.8.0
+to 2.8.4 essentially concern the tina tool:
+
+- New tina  modes (tina -D/-F/-F1) provides three  variants of Louchka
+Popova's "essential states" construction;
+
+- Constructions  -S,  -A and  -U  have  been  improved for  nets  with
+unbounded firing  intervals: instead of the  "clock domain relaxation"
+defined in our TACAS'03 paper, these constructions now use the simpler
+"normalization" operation proposed by Hadjidj/Boucheneb;
+
+- A variant of  the coverability tree construction (-Cm  n) allows one
+to set a marking threshold for unbounded places (see the man pages for
+details);
+
+Though this is  not documented yet, Tina 2.8.4  also supports (for all
+targets) a  form of "predicate/action" Time Petri  net: predicates and
+actions over  some data  may be associated  with the transitions  of a
+net, written in C. Some tutorial examples are available.
+
+Finally, an experimental version  of Tina is available, called SwTina.
+SwTina supports  an extension of  Time Petri nets with  suspension and
+resumption of transitions, called "Stopwatch Time Petri nets".  Please
+check  the  page   http://www.laas.fr/tina/next.php  for  details  and
+pointers.
+
+
+Changes from 2.7.4 to 2.8.0:
+-----------------------------
+
+tina-2.8.0 brings a number of new features and three new tools, all
+brielfly described below.
+
+PNML support:
+=============
+
+(check doc/formats/pnml.txt for futher information)
+
+Tina 2.8.0 provides a preliminary  support for PNML. PNML support will
+follow evolutions of the PNML  standard. The version of PNML currently
+supported  are  BasicPNML   and  its  extension  (TPNPNML)  informally
+described below. The TPNPNML extends Basic PNML as follows:
+
+- In the "graphics" element of a node, one may add an offset specification
+  interpreted as the position of the node id, relative to the node.
+  e.g.	<offset x=... y=... />
+
+- arcs may have an optional "type" element, one of normal, inhibitor, test;
+  e.g.	<type value="test"/>
+
+- Any transition may have a "delay" element, specifying a time interval in
+  the style of MathML intervals, and optionally some position relative to
+  the transition.
+
+  e.g. (check doc/formats/pnml.txt for other examples) interval [4,9],
+  positionned (-10,0) relative to the transition is specified as follows
+  (note the "closure" attribute in the interval line):
+
+  <delay>
+   <interval xmlns="http://www.w3.org/1998/Math/MathML" closure="closed">
+    <cn>4</cn>
+    <cn>9</cn>
+   </interval>
+   <graphics>
+    <offset x="-10" y="0" />
+   </graphics>
+  </delay>
+
+The tools tina, struct, and the new plan tool, natively read BasicPNML
+and its above extension. The nd editor may import from, and export to,
+the above  format. The new ndrio  tool can convert  between .pnml .ndr
+and .net formats. PNML support will follow evolutions of the PNML standard.
+
+Generalized inhibitor arcs and test (read) arcs:
+================================================
+
+All tools now support generalized inhibitor arcs and test (read) arcs.
+The .aut and .ndr formats have been extended to support these features
+(check   formats/net.txt   and   formats/ndr.txt   for  up   to   date
+descriptions).  The .pnml TPN format also supports these.
+
+To specify  a test (resp.   inhibitor) arc in  .net or .ndr,  one must
+specify  its weight  and  uses  "?"  (resp.   "-?")   instead of  "*".
+e.g. in  the following line,  p1*3 defines a  normal arc of  weight 3,
+p2?4 a test arc of weight 4, and p3?-2 an inhibitor arc of weight 2.
+
+   tr t1 p1*3 p2?4 p3?-2 -> p4*5
+   tr t2 p2?4 p5 -> p6
+
+In the nd graphic editor, clicking  <3> on an arc allows to select its
+type together with its weight.
+
+NOTE: The boundedness proprety  is undecidable for nets with inhibitor
+arcs. However,  tina still  uses the usual  stopping test  by default,
+that provides  here a sufficient  only condition for  boundedness.  If
+desired, one  one may cancel it  (option -s 0) and  optionnaly use the
+limit flags to enforce termination.
+
+The net scripting language tpn:
+===============================
+
+In  addition to  format .net,  .ndr and  .pnmml, the  tina-2.8.0 tools
+support a  simple scripting language  for building Time Petri  nets by
+composition of  smaller nets.
+
+The  .tpn  format   extends  both  .net  and  .ndr,   its  syntax  and
+interpretation are defined in  file formats/tpn.txt. In short, the tpn
+format allows one to build nets by composing net elements specified in
+.net and/or  .ndr, composition operations  rely upon the .net  or .ndr
+labels. When nd,  tina, or another tool, reads a  .tpn files, the file
+is interpreted on the fly. The composition operations are:
+
+   - merge n : juxtaposition of nets (without fusion)
+   - sync n  : composition by transitions (synchronous)
+   - chain n : composition by places
+   - ren ... : renaming and hiding of labels
+
+The .tpn  format will  probably be extended  in future  versions. Some
+example nets can be found in directory nets/tpn_examples.
+
+New syntax for defining labels in .net:
+=======================================
+
+A mode convenient syntax is provided for declaring place or transition
+labels in .net  files.  That notation will replace  in future releases
+the obsolete "lb" declarations. e.g.
+
+to assign label {TRANS 34} to transition t1, one had to write in 2.7.4:
+
+		tr t1 [3,4[ p1 -> p2
+                lb t1 {TRANS 34}
+	
+In 2.8.0, these two lines are equivalent to:
+
+		tr t1 : {TRANS 34} [3,4[ p1 -> p2
+	
+Changes to the tina tool:
+=========================
+
+In addition to  the support of PNML, and  inhibitor/read arcs, two new
+flags, -lt  and -ls  allows one to  output transition systems  (in any
+output format) labelled by node labels rather than node names. This is
+particularly useful in conjunction with CADP.
+
+Also, performances have been improved for all constructions, specially
+for nets with a large number of transitions.
+
+Changes to the struct tool:
+===========================
+
+Now accepts  net descriptions  in .pnml or  .tpn formats as  well (see
+above).  Structural analysis is performed on nets with their inhibitor
+and read arcs removed.
+
+New tool, selt:
+===============
+
+This new tool is a model checker for a variant of State/Event-LTL with
+integer  state/transition properties.  The  tool operates  on extended
+Kripke transition systems in .ktz format (as built by tina with option
+-k), and model  checks the ktz read against  extended S/E-LTL formula.
+To give an idea, the following  are examples of legal selt commands:
+
+    [] (3*p1 + 4*p2 - p3 >= 7);	         (checks a marking invariant)
+    infix x follows y = [] (y => <> x);  (declares follows)
+    t5 follows (p5 >= 4);		 (a mixed state/trans formula)
+
+Check the  selt man page (doc/man/mann/selt.n)  or in doc/txt/selt.txt
+for a full description.
+
+For  translation of  LTL formula  to  Buchi automata,  selt relies  on
+ltl2ba,   a    tool   developped    by   Didier   Oddoux    at   Liafa
+(http://www.liafa.jussieu.fr/~oddoux).
+
+New tool, ndrio:
+================
+
+This new tool converts between net descriptions in formats .net, .ndr,
+.tpn and  .pnml. When  converting from a  textual format to  a graphic
+one, a drawing  tool may be specified (one  of graphplace, dot, neato,
+circo).
+
+Check   the   ndrio   man   page   (doc/man/mann/ndriot.n)   or   file
+doc/txt/ndrio.txt for a full description.
+
+New tool, plan:
+==============
+
+This  tool  accepts  as  arguments  a net  and  a  firable  transition
+sequence, and, according to other options, produces a characterisation
+of all firing  schedules having this sequence as  support, or a single
+such  firing   schedule.  This  tool  is   particularly  helpful  when
+model-checking  Time Petri nets,  it allows  to transform  the untimed
+counter examples produced by selt into firable firing schedules (times
+firing sequences) loadable into the nd simulator for replay.
+
+---------------------------------------------------------------------------
+
+CHANGES from V2.7.2 to 2.7.4:
+-----------------------------
+
+2.7.4  mainly improves  the  nd editor  and  stepper simulator.  Also,
+installation on Windows is simpler. The changes are:
+
+* [nd]   Now   provides   selection,   with  standard   bindings   and
+Cut/Copy/Paste/Move facilities for node groups.
+
+* [nd]   Several  nets  can   be  merged   into  the   graphic  buffer
+(File->include->...).
+
+* [nd] Nodes in the graphic  buffer can be fused (superpose them, then
+use Button 3);
+
+* [nd]   Generic  facilities   allows  one   to  invoke   his/her  own
+applications from  the tools menu,  provided they operate on  files in
+the formats recognized by nd, check (Tools->how to ...) for details.
+
+Available plugins  for nd using  these features will be  advertized in
+the new Friends page, if desired.
+
+* [nd]  The  stepper  simulator  has  been  much  improved,  in  look,
+behavior, and functions for replaying scenarios
+
+* [tools]  On windows,  the cygwin  library  is no  more needed,  just
+download and run.
+
+* [tools]: A new flag (-wp) controls generation of temporal divergence
+information in lts outputs (check  the man pages for details). The ktz
+format captures that information.
+
+
+---------------------------------------------------------------------------
+
+CHANGES from V2.7.0 to 2.7.2:
+-----------------------------
+
+For Linux/Windows/Solaris, 2.7.2 is  essentially a bug fixes and clean
+up release.  The real novelty is  availability of a  version for MacOS
+X. The changes are:
+
+* [nd+tools] Now available for MacIntoshes  under MacOS X. The MacOS X
+release comes with two versions of the editor, one runs under X11, and
+the  other runs  under  the  native Aqua  graphic  system. Check  file
+INSTALL in the distribution for details.
+
+* [nd]  Now runs  with the  latest,  and much  faster, Tcl/Tk  version
+8.4. To ease installation, the editor  is now deployed as a standalone
+application  only. Problems  with management  of temporary  files have
+been solved.
+
+
+
+---------------------------------------------------------------------------
+
+CHANGES FROM V2.6,. to V2.7.0 :
+-------------------------------
+
+Version 2.7.0  brings major  improvements over previous  releases. The
+major changes are:
+
+* [nd] Includes  a stepper simulator. One  may animate a  Petri net or
+Time Petri net without leaving the editor;
+
+* [tina and struct] Overall  performances improvements due to a change
+of compiler.   
+
+* [tools] Installation  and command line usages are  easier since tina
+and struct are now standalone executables;
+
+* [tina]  Improved algorithmics  for  constructions -S  (SSCG) and  -A
+(ASCG);
+
+* [tina] New modes -M (preserves markings), -E (preserves states), and
+-Vq (checks quasi-liveness);
+
+* [struct] Now  offers a choice  of algorithms for computing  flows or
+semiflows;
+
+
+---------------------------------------------------------------------------
+
+CHANGES FROM V2.0 to V2.6.6:
+---------------------------
+
+(dropped)
+
+
+---------------------------------------------------------------------------
+

tools/tina-3.7.0/INSTALL

+Installation instructions for Linux or Solaris.
+
+
+1. prerequisites:
+-----------------
+
+None.
+
+
+2. installing the toolbox:
+--------------------------
+
+Download and  unpack the tina  distribution. This creates  a hierarchy
+rooted  at tina-3.X.Y.   The binaries  are in  subdirectory  bin.  The
+editor  is "nd".
+
+The man pages are in  doc/man/mann, a quick installation in tcsh is e.g.
+	setenv MANPATH <tinadir>/doc/man:$MANPATH
+Directory doc/txt holds text only copies of these.
+
+To  use  the tools  standalone,  you  may wish  to  add  the tina  bin
+directory to the PATH environment variable, and the tina lib directory
+(if any) to  variable LD_LIBRARY_PATH. This is not  required for using
+the tools from  the editor, however.  Alternatively, nd  and the tools
+can  be  moved or  copied  at  some  standard place  (e.g.   /usr/bin)
+provided all the contents of the tina bin directory is moved or copied
+there. Similarly, the libraries could be moved to /usr/lib and the man
+pages to /usr/man/mann.
+
+The nd  graphic editor assumes  a 3-button mouse is  present. Bindings
+for  emulating a  3-button  mouse with  a  2-button mouse  or pad  are
+built-in: the  Middle button is simulated  by Shift-RightButton. Click
+Help->nd help for information on the graphic bindings.
+
+
+3. drawing filters:
+-------------------
+
+Nd can draw nets or  automata from textual descriptions, provided some
+placement filters  are installed.  Nd has builtin  interfaces for four
+filters :  graphplace, dot, neato  and circo. Graphplace and  dot play
+somewhat the  same role  and are suitable  for drawing dags;  neato is
+best suited for drawing graphs  with cycles; circo attempts a circular
+layout.
+
+Graphplace is bundled  with nd. It is a program  by Jos van Eijndhoven
+at Eindhoven University of Technology, available in source form at:
+	ftp://ftp.es.ele.tue.nl/pub/users/jos/graphplace.tar.gz
+
+Filters  dot, neato  and  circo are  part  of the  AT&T graph  drawing
+package  Graphviz.  Graphviz  is  available  precompiled  for  various
+platforms at:
+	http://www.graphviz.org
+
+For convenience,  stripped down versions  of dot, neato and  circo are
+bundled with the tina distributions.  If Graphviz is already installed
+on your system,  then you may wish to delete the  versions in the tina
+bin directory, and make the installed filters reachable from your PATH
+instead.
+
+
+4. bcg support:
+---------------
+
+Format  bcg  is one  of  the formats  supported  by  the CADP  toolbox
+(available at http://www.inrialpes.fr/vasy/cadp).  Bcg support is only
+available on linux and windows versions (please contact us if you need
+bcg support for other targets).  It first requires to properly install
+the CADP  toolset on your machine,  then you must  compile and install
+libbcg.so  (on linux),  or  libbcg.dll (on  windows)  as explained  in
+extras/bcgsupport/README.
+
+
+5. pnml support:
+----------------
+
+As  of 2.8.0,  the  tina tools  support  the PNML  (Petri Nets  Markup
+Language) format as  an alternative to .net or  .ndr. The PNML support
+is still evolving,  check the formats man page  for details about PNML
+support by tina.
+
+
+6. help, feedback:
+------------------
+
+Please report bugs or other problems to the author at bernard@laas.fr.
+All comments/questions are also welcome on the tina-users forum:
+
+	register at url: http://sympa.laas.fr/wws/info/tina-users
+	post at address: tina-users@laas.fr	
+
+Enjoy,