ProjectionDiagram: Difference between revisions

No edit summary
(Update links where possible)
 
(4 intermediate revisions by one other user not shown)
Line 3: Line 3:
This page provides additional resources for the paper we have submitted for the [http://icfem2015.lri.fr/ ICFEM 2015].
This page provides additional resources for the paper we have submitted for the [http://icfem2015.lri.fr/ ICFEM 2015].


=== ProB Live Visualisations ===
=== Resources and ProB Live Visualizations ===


We have prepared two interactive live visualizations. One of the Event-B model of the landing gear system (the full description of the case study can be found [[Media:landing_system.pdf|here]]) and one of the Event-B model of a simple lift system.
We have prepared two interactive live visualizations. One of the Event-B model of the landing gear system (the full description of the case study can be found [[Media:landing_system.pdf|here]]) and one of the Event-B model of a simple lift system.
Line 9: Line 9:
The visualizations can either be controlled by interacting with the displayed elements (i.e., clicking the handle) or using the Events view which can be opened using the "Open View" menu at the bottom right corner.  
The visualizations can either be controlled by interacting with the displayed elements (i.e., clicking the handle) or using the Events view which can be opened using the "Open View" menu at the bottom right corner.  


# [http://cobra.cs.uni-duesseldorf.de:18081/landing.html Visualization of the landing gear system]
# [http://wyvern.cs.uni-duesseldorf.de/bms/landing.html Visualization of the landing gear system]
# [http://cobra.cs.uni-duesseldorf.de:18081/lift.html Visualization of the simple lift]
# [http://wyvern.cs.uni-duesseldorf.de/bms/lift.html Visualization of the simple lift]


The Event-B model of the simple lift system be can be downloaded here: [[File:SimpleLift.zip]].


==== Creating a Projection on Graphical Elements ====
[https://www.cs.hhu.de/lehrstuehle-und-arbeitsgruppen/softwaretechnik-und-programmiersprachen/publikationen#LadenbergerLeuschel_ProjectDiagram Technical Report]
 
==== Creating a Domain Specific Projection ====


* Open the ModelCheckingUI  using the "Open View" menu at the bottom right corner.
* Open the ModelCheckingUI  using the "Open View" menu at the bottom right corner.
Line 20: Line 23:
* Select the lift or landing visualization respectively and select some elements for the projection.
* Select the lift or landing visualization respectively and select some elements for the projection.


Please note: Due to a small bug, you can only create a projection for max. two selected graphical elements at the moment. We are already working on this bug.  
Please note: Due to a small bug, you can only create a projection for max. two selected graphical elements at the moment. We are already working on this bug.


=== Links ===
=== Links ===


==== BMotion Studio for ProB ====
==== BMotion Studio for ProB ====
* [http://www.stups.hhu.de/ProB/index.php5/BMotion_Studio BMotion Studio for ProB Homepage]
* [[BMotion Studio|BMotion Studio for ProB Homepage]]
* [http://nightly.cobra.cs.uni-duesseldorf.de/bmotion/bmotion-prob-handbook/nightly/html/ BMotion Studio for ProB User Handbook]
* [https://stups.hhu-hosting.de/handbook/bmotion/current/html/ BMotion Studio for ProB User Handbook]
* [https://github.com/ladenberger/bmotion-prob BMotion Studio for ProB Sourcecode]
* [https://github.com/ladenberger/bmotion-prob BMotion Studio for ProB Sourcecode]


==== ProB 2.0 ====
==== ProB 2.0 ====
* [http://nightly.cobra.cs.uni-duesseldorf.de/prob2/prob2-handbook/nightly/devel/html/ ProB 2.0 Developer Handbook]
* [https://stups.hhu-hosting.de/handbook/prob2/prob_handbook.html ProB 2.0 Developer Handbook]
* [https://github.com/bendisposto/prob2 ProB 2.0 Sourcecode]
* [https://github.com/hhu-stups/prob2_kernel ProB 2.0 Sourcecode]
* [http://nightly.cobra.cs.uni-duesseldorf.de/experimental/updatesite/ ProB 2.0 Nightly Build Updatesite]
* [https://stups.hhu-hosting.de/rodin/prob2/nightly/ ProB 2.0 Nightly Build Updatesite]
* [[Tutorial13|ProB 2.0 Tutorial]]
* [[Tutorial13|ProB 2.0 Tutorial]]
=== References ===
<references/>

Latest revision as of 12:50, 23 February 2023


This page provides additional resources for the paper we have submitted for the ICFEM 2015.

Resources and ProB Live Visualizations

We have prepared two interactive live visualizations. One of the Event-B model of the landing gear system (the full description of the case study can be found here) and one of the Event-B model of a simple lift system.

The visualizations can either be controlled by interacting with the displayed elements (i.e., clicking the handle) or using the Events view which can be opened using the "Open View" menu at the bottom right corner.

  1. Visualization of the landing gear system
  2. Visualization of the simple lift

The Event-B model of the simple lift system be can be downloaded here: File:SimpleLift.zip.

Technical Report

Creating a Domain Specific Projection

  • Open the ModelCheckingUI using the "Open View" menu at the bottom right corner.
  • Click on the "MC" icon and run the model checker in order to explore the full state space of the model.
  • After finishing, you can open the Element Projection view using the "Open Diagram" menu at the bottom right corner.
  • Select the lift or landing visualization respectively and select some elements for the projection.

Please note: Due to a small bug, you can only create a projection for max. two selected graphical elements at the moment. We are already working on this bug.

Links

BMotion Studio for ProB

ProB 2.0