ProR - Revision history

imported>Ladenberger: /* Roadmap */

2013-06-21T10:04:27Z

Roadmap

← Older revision		Revision as of 10:04, 21 June 2013
Line 82:		Line 82:
	=== Roadmap ===		=== Roadmap ===

	*There are still some limitations on the ProR/Rodin integration plugin, however. While all required data structures exist, the plugin would benefit from more sophisticated reporting. In particular, <ref>http://www.stups.uni-duesseldorf.de/w/~~Special:Publication~~/~~HalJasLad2012~~</ref> lists a number of properties of a correct system description. While the presence of these properties does not guarantee correctness, their absence indicates a problem. Reporting on the state of these properties would be valuable.		*There are still some limitations on the ProR/Rodin integration plugin, however. While all required data structures exist, the plugin would benefit from more sophisticated reporting. In particular, <ref>http://www.stups.uni-duesseldorf.de/mediawiki/images/e/ec/Pub-HalJasLad2013.pdf</ref> lists a number of properties of a correct system description. While the presence of these properties does not guarantee correctness, their absence indicates a problem. Reporting on the state of these properties would be valuable.

	*<del>Furthermore, the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.</del>		*<del>Furthermore, the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.</del>

imported>Ladenberger: /* Roadmap */

2013-03-05T15:32:24Z

Roadmap

← Older revision		Revision as of 15:32, 5 March 2013
Line 86:		Line 86:
	*<del>Furthermore, the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.</del>		*<del>Furthermore, the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.</del>

	*Jump to Rodin Editor ~~when double-clicking on a Link~~		*<del>Jump to Rodin Editor via context menu</del>

	= References =		= References =
	<references/>		<references/>

imported>Ladenberger: /* Roadmap */

2013-03-05T13:08:01Z

Roadmap

← Older revision		Revision as of 13:08, 5 March 2013
Line 82:		Line 82:
	=== Roadmap ===		=== Roadmap ===

	There are still some limitations on the ProR/Rodin integration plugin, however. While all required data structures exist, the plugin would benefit from more sophisticated reporting. In particular, <ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/HalJasLad2012</ref> lists a number of properties of a correct system description. While the presence of these properties does not guarantee correctness, their absence indicates a problem. Reporting on the state of these properties would be valuable.		*There are still some limitations on the ProR/Rodin integration plugin, however. While all required data structures exist, the plugin would benefit from more sophisticated reporting. In particular, <ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/HalJasLad2012</ref> lists a number of properties of a correct system description. While the presence of these properties does not guarantee correctness, their absence indicates a problem. Reporting on the state of these properties would be valuable.

	<del>Furthermore, the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.</del>		*<del>Furthermore, the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.</del>

			*Jump to Rodin Editor when double-clicking on a Link

	= References =		= References =
	<references/>		<references/>

imported>Ladenberger: /* Roadmap */

2013-03-05T13:03:43Z

Roadmap

← Older revision		Revision as of 13:03, 5 March 2013
Line 84:		Line 84:
	There are still some limitations on the ProR/Rodin integration plugin, however. While all required data structures exist, the plugin would benefit from more sophisticated reporting. In particular, <ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/HalJasLad2012</ref> lists a number of properties of a correct system description. While the presence of these properties does not guarantee correctness, their absence indicates a problem. Reporting on the state of these properties would be valuable.		There are still some limitations on the ProR/Rodin integration plugin, however. While all required data structures exist, the plugin would benefit from more sophisticated reporting. In particular, <ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/HalJasLad2012</ref> lists a number of properties of a correct system description. While the presence of these properties does not guarantee correctness, their absence indicates a problem. Reporting on the state of these properties would be valuable.

	Furthermore, the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.		<del>Furthermore, the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.</del>

	= References =		= References =
	<references/>		<references/>

imported>Ladenberger: /* How to install? */

2012-08-28T08:21:06Z

How to install?

← Older revision		Revision as of 08:21, 28 August 2012
Line 17:		Line 17:
	The ProR Rodin Integration is installed via an update site. Starting with Rodin 2.5, the update site for the integration plugin is already included. Otherwise, here are the current available update sites:		The ProR Rodin Integration is installed via an update site. Starting with Rodin 2.5, the update site for the integration plugin is already included. Otherwise, here are the current available update sites:

	Update Site: http://~~www~~.~~stups~~.~~uni-duesseldorf.de/pror_updates~~		Update Site: http://update.formalmind.com/rodin

	~~Nightly Build: http://www.stups.uni-duesseldorf.de~~/~~pror_nightly~~

	=== Tutorial ===		=== Tutorial ===

imported>Ladenberger at 14:11, 27 June 2012

2012-06-27T14:11:28Z

← Older revision		Revision as of 14:11, 27 June 2012
Line 87:		Line 87:

	Furthermore, the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.		Furthermore, the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.

			= References =
			<references/>

imported>Ladenberger at 14:10, 27 June 2012

2012-06-27T14:10:46Z

← Older revision		Revision as of 14:10, 27 June 2012
Line 81:		Line 81:
	* <del>Terminating editing with a carriage return inserts a linebreak. Better finish editing by clicking outside the cell.</del>		* <del>Terminating editing with a carriage return inserts a linebreak. Better finish editing by clicking outside the cell.</del>
	* Renaming the Event-B project will destroy the created links. You have to open the ReqIF file with a text editor and replace the old Event-B project name with the new one at the corresponding places.		* Renaming the Event-B project will destroy the created links. You have to open the ReqIF file with a text editor and replace the old Event-B project name with the new one at the corresponding places.

			=== Roadmap ===

			There are still some limitations on the ProR/Rodin integration plugin, however. While all required data structures exist, the plugin would benefit from more sophisticated reporting. In particular, <ref>http://www.stups.uni-duesseldorf.de/w/Special:Publication/HalJasLad2012</ref> lists a number of properties of a correct system description. While the presence of these properties does not guarantee correctness, their absence indicates a problem. Reporting on the state of these properties would be valuable.

			Furthermore, the plugin does not support classifying phenomena. In a next step we will work on a concept for classifying and maintaining phenomena with ProR.

imported>Ladenberger: /* Known Problems */

2012-05-14T13:26:07Z

Known Problems

← Older revision		Revision as of 13:26, 14 May 2012
Line 77:		Line 77:
	=== Known Problems ===		=== Known Problems ===

	* Pasting (and copying) in the cell with the highlighting is currently not possible. A workaround is to temporarily disable the corresponding plug-in. Then copy and paste works, but only through the context menu.		* <del>Pasting (and copying) in the cell with the highlighting is currently not possible. A workaround is to temporarily disable the corresponding plug-in. Then copy and paste works, but only through the context menu.</del>
	* ReqIF Files are currently not shown in the Rodin Explorer. To see (and open), please use the Navigator View instead.		* <del>ReqIF Files are currently not shown in the Rodin Explorer. To see (and open), please use the Navigator View instead.</del>
	* Terminating editing with a carriage return inserts a linebreak. Better finish editing by clicking outside the cell.		* <del>Terminating editing with a carriage return inserts a linebreak. Better finish editing by clicking outside the cell.</del>
			* Renaming the Event-B project will destroy the created links. You have to open the ReqIF file with a text editor and replace the old Event-B project name with the new one at the corresponding places.

imported>Ladenberger: /* Tracking Changes */

2012-05-14T13:21:47Z

Tracking Changes

← Older revision		Revision as of 13:21, 14 May 2012
Line 72:		Line 72:

	When traced formal model elements change, the trace is marked as “suspect” by showing a small icon. Two columns exist for the source and the target of the trace, respectively. The user sees at a glance which requirements or formal model elements need to be revalidated. This is particularly useful if the requirements document becomes large. By double-clicking on the “suspect” icon, the user can mark the trace as “revalidated’’ and the icon will be removed.		When traced formal model elements change, the trace is marked as “suspect” by showing a small icon. Two columns exist for the source and the target of the trace, respectively. The user sees at a glance which requirements or formal model elements need to be revalidated. This is particularly useful if the requirements document becomes large. By double-clicking on the “suspect” icon, the user can mark the trace as “revalidated’’ and the icon will be removed.

			[[Image:pror_rodin_4.png]]

	=== Known Problems ===		=== Known Problems ===

imported>Ladenberger: /* Creating Links from Event-B to ProR */

2012-05-14T13:20:38Z

Creating Links from Event-B to ProR

← Older revision		Revision as of 13:20, 14 May 2012
Line 41:		Line 41:
	==== Creating Links from Event-B to ProR ====		==== Creating Links from Event-B to ProR ====

	Simply drag Event-B elements from the Event-B Explorer (you can unfold models there) right into the Specification Editor. This will create a trace. In order to see the created traces, you have to click on the small "triangle" icon in the tool bar menu.		Manual creation of traces between requirements and formal model elements is supported via drag and drop. Simply drag Event-B elements from the Event-B Explorer (you can unfold models there) right into the Specification Editor. This will create a trace. In order to see the created traces, you have to click on the small "triangle" icon in the tool bar menu.

			The right column “Link” of the specification editor summarizes the number of outgoing (target) and incoming (source) traces. Selecting an outgoing trace shows the targets properties in the Properties View. In addition, traces can be annotated if additional information is necessary.

	[[Image:pror_rodin_2.png]]		[[Image:pror_rodin_2.png]]