Find research datasets worth reusing
Search datasets from major research repositories and use ShareScore to quickly assess how well each record supports discovery, access, and reuse.
5
datasets available to search
ShareScore release 0.9.0
Dataset results
5 results for “Colored Petri Net”
Automatic message sequence chart creation from simulation run of the parametric colored Petri net model of the Chandy-Lamport algorithm with four processes
<p><span>The video shows the creation of the message sequence chart from a simulation run of the proposed parametric colored Petri net model of the Chandy-Lamport algorithm using the CPN tool with four constituting processes. The picture shows the resulting message sequence chart. </span></p> <p><strong><span>Message Sequence Chart of Parametric Model With 4 Processes via Automatic Simulation Run_SuppInfo.mp4</span></strong><span>: This video shows the automatic generation of a message sequence chart of the proposed parametric colored Petri net model of the Chandy-Lamport distributed global snapshot algorithm using the CPN tool version 4.0.0. The model's number of constituting processes is parametric and was set to four. The video was generated using the authors' updated CPN tool extension server. The automatic simulation run of the model has been used to create this video. The CPN tool randomly selects the enabled transition at each step in an automatic simulation run.</span></p> <p><strong><span>Picture of Message Sequence Chart of Parametric Model With 4 Processes_SuppInfo.png:</span></strong><span> This picture shows the automatically generated message sequence chart of the proposed parametric colored Petri net model of the Chandy-Lamport algorithm that is visible in the above video clip. The number of constituting processes was set to four. </span></p>
Automatic message sequence chart creation from simulation run of the Chandy-Lamport algorithm modeled by colored Petri net
<p>Videos of two message sequence chart creation from simulation runs of the Chandy-Lamport algorithm modeled by colored Petri net using the CPN tool.</p> <p><strong>Message Sequence Chart Of Model With Automatic Simulation Run_SuppInfo.mp4</strong>: This video shows the automatic generation of a message sequence chart of a proposed colored Petri net model of the Chandy-Lamport distributed global snapshot algorithm using the CPN tool version 4.0.1. The video has been generated by the authors' updated extension server of the CPN tool. The automatic simulation run of the model has been used to create this video. The CPN tool randomly selects the enabled transition in an automatic simulation run.</p> <p><strong>Message Sequence Chart Of Model With Step-By-Step Simulation Run_SuppInfo.mp4:</strong> This video shows the automatic generation of a message sequence chart of the proposed colored Petri net model of the Chandy-Lamport algorithm in a step-by-step simulation run with our updated extension server of the CPN tools version 4.0.1. We fired our selected enabled transition of the model to create this video.</p>
Model checking of Chandy-Lamport algorithm modeled by colored Petri net
<p>This video shows model checking of a proposed colored Petri net model of the Chandy-Lamport distributed global snapshot algorithm using the CPN tool version 4.0.1. It shows the functions and codes written in ML language and the result of calling them used for model checking the proposed model's state space graph. The last ML code at the end of the page, named state space, does whole model checking and operates using previously displayed codes and functions. This video aimed to demonstrate the steps of our proposed model checking.</p>
Model checking of the proposed parametric colored Petri net model of the Chandy-Lamport algorithm
<p>This video shows model checking of a proposed parametric colored Petri net model of the Chandy-Lamport distributed global snapshot algorithm using the CPN tool version 4.0.0. The number of constituting processes is parametric in this model. It shows the functions written in ML language and the result of calling them for customized analysis of the proposed model's state space graph. The last ML code at the end of the page, "state space," summarizes the model checking and operates by calling previously displayed functions. This video aimed to demonstrate the proposed verification process of the parametric model.</p>
Automatic message sequence chart creation from simulation run of the proposed parametric colored Petri net model of the Chandy-Lamport algorithm
<p><span>These videos show the creation of two message sequence charts from simulation runs of the proposed parametric colored Petri net model of the Chandy-Lamport algorithm using the CPN tool with three constituting processes. </span></p> <p><strong><span>Message Sequence Chart of <span> </span>Parametric Model With 3 Processes via Automatic Simulation Run_SuppInfo.mp4</span></strong><span>: This video shows the automatic generation of a message sequence chart of the proposed parametric colored Petri net model of the Chandy-Lamport distributed global snapshot algorithm using the CPN tool version 4.0.0. The number of constituting processes is parametric in the model and was set to three. The video was generated using the authors' updated CPN tool extension server. The automatic simulation run of the model has been used to create this video. The CPN tool randomly selects the enabled transition at each step in an automatic simulation run.</span></p> <p><strong><span>Message Sequence Chart of Parametric Model With 3 Processes via Step-By-Step Simulation Run_SuppInfo.mp4:</span></strong><span> This video shows the automatic generation of a message sequence chart of the proposed parametric colored Petri net model of the Chandy-Lamport algorithm in a step-by-step simulation run with our updated extension server of the CPN tools version 4.0.0. The number of constituting processes is parametric in the model and was set to three. We manually fired our selected enabled transition of the model to create this video. </span></p>
ScienceDex guides
Understand access before you commit
These curated guides explain access requirements, typical timelines, costs, and reuse considerations for widely used research datasets.
Allen Brain Atlas
Allen Brain Atlas is an Allen Institute collection of brain map atlases, datasets, APIs, and analysis tools covering mouse, human, and non-human primate brain resources.
Annotated Behaviour and Observability Dataset (ABODe)
ABODe is a University of Edinburgh DataShare dataset for behavior classification in group-housed mice using home-cage video, identities, bounding boxes, ground-plate positions, and annotator labels.
DANDI Archive for NWB datasets
DANDI is a BRAIN Initiative archive for publishing and sharing neurophysiology data, including electrophysiology, optophysiology, and behavioral data packaged as NWB and related standards.
International Brain Laboratory public data
The International Brain Laboratory public data releases expose standardized mouse decision-making experiments, including Neuropixels recordings, widefield calcium imaging, behavior, and session metadata accessed through the ONE API.
OpenNeuro
OpenNeuro is a free, open platform for sharing neuroimaging datasets, with public search, dataset pages, and download paths for web, S3, DataLad, and the OpenNeuro CLI.