ProB Java API Tutorial - Revision history

David Geleßus: Update links

2023-02-23T12:42:40Z

Update links

← Older revision		Revision as of 12:42, 23 February 2023
Line 5:		Line 5:
	== How to get started developing with ProB 2.0 ==		== How to get started developing with ProB 2.0 ==

	The source code for ProB 2.0 is ~~available via GitHub. Click~~ [https://github.com/~~bendisposto~~/~~prob2 here~~] ~~to view the prob2 repository~~. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. ~~Our bugtracker is available~~ [~~http~~://~~jira~~.~~cobra.cs.uni~~-~~duesseldorf.de~~/~~browse~~/~~PROBCORE here~~]~~. There~~ you can view the features that we are currently working on and can submit new feature requests.		The source code for ProB 2.0 is [https://github.com/hhu-stups/prob2_kernel available via GitHub]. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. On [https://github.com/hhu-stups/prob-issues/issues our bug tracker], you can view the features that we are currently working on and can submit new feature requests.

	== How to open the Groovy Shell ==		== How to open the Groovy Shell ==

Michael Leuschel: /* How to animate with only the StateSpace abstraction */

2017-09-26T07:48:31Z

How to animate with only the StateSpace abstraction

← Older revision		Revision as of 07:48, 26 September 2017
Line 218:		Line 218:

	So you can execute anyEvent with the method anyEvent(filter), where filter can be a String name, or a List of names. You can also execute an event with name "name", with the method name(predicate), where predicate is the predicate string intended to filter the solutions for the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added.		So you can execute anyEvent with the method anyEvent(filter), where filter can be a String name, or a List of names. You can also execute an event with name "name", with the method name(predicate), where predicate is the predicate string intended to filter the solutions for the event. If there are no parameters, the predicate "TRUE = TRUE" will automatically be added.


			== How to use a different probcli binary for ProB2 ==

			You need to start ProB2 or the respective Java application with:
			-Dprob.home=PATHTOPROBCLIFOLDER

Joy Clark: /* How to run a groovy script */

2014-11-05T15:08:58Z

How to run a groovy script

← Older revision		Revision as of 15:08, 5 November 2014
Line 201:		Line 201:
	You can use the build in <tt>run</tt> command to run a groovy script. Simply type		You can use the build in <tt>run</tt> command to run a groovy script. Simply type

	<tt> run pathToScript/script.groovy </tt>		<tt> run new File(pathToScript/script.groovy) </tt>

	into the console~~. Code completion is available for the run command~~.		into the console.

	== How to animate with only the StateSpace abstraction ==		== How to animate with only the StateSpace abstraction ==

Joy Clark: /* How to convert between the main abstractions */

2014-11-05T15:08:28Z

How to convert between the main abstractions

← Older revision		Revision as of 15:08, 5 November 2014
Line 169:		Line 169:
	<tt> model = trace as EventBModel </tt> or <tt> model = trace as ClassicalBModel </tt>		<tt> model = trace as EventBModel </tt> or <tt> model = trace as ClassicalBModel </tt>

	The only thing to mention is that every time you convert from a StateSpace or Model to a Trace, a new trace is created.		The only thing to mention is that every time you convert from a StateSpace or Model to a Trace, a new trace from the root state is created.

	== How to save a trace ==		== How to save a trace ==

Joy Clark: /* How to carry out evaluations */

2014-11-05T15:08:03Z

How to carry out evaluations

← Older revision		Revision as of 15:08, 5 November 2014
Line 121:		Line 121:
	It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the Trace and the StateSpace. In the trace, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,		It is very simple to evaluate strings in the groovy console. There is a build in eval method in both the Trace and the StateSpace. In the trace, you just need to specify a string and the parser that is needed to parse the string. The two parsers currently available are <tt>ClassicalB</tt> and <tt>EventB</tt>.For instance,

	<tt> t.~~eval~~("x:NAT" as EventB) </tt>		<tt> t.evalCurrent("x:NAT" as EventB) </tt>

	will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code		will parse "x:NAT" using the Event B parser and then will evaluate it at the current state. The following code

	<tt> t.~~eval~~("x:NAT" as ClassicalB) </tt>		<tt> t.evalCurrent("x:NAT" as ClassicalB) </tt>

	will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.		will parse "x:NAT" using the Classical B parser and then will evaluate it at the current state.

	~~Classical B is actually~~ the ~~default~~ parser, ~~so it would also~~ be ~~sufficient to write~~		The Trace class can also attempt to identify the correct parser for the formula in question. This means that for an EventBModel the EventB parser will be used, and for a ClassicalBModel, the ClassicalB parser will be used. In this case, calling the evalCurrent method with a String parameter will parse the String formula with the parser associated with the current formalism being animated. In this case

	<tt> t.eval("x:NAT")</tt>.		<tt> t.eval("x:NAT")</tt>.

			will identify which model type is being animated and choose the appropriate parser.

	It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing		It is also possible to evaluate formulas on the SpaceSpace level. For instance, if <tt>space_0</tt> is a StateSpace, you can evaluate a list of formulas by typing

Joy Clark: /* In The Console */

2014-11-05T15:04:08Z

In The Console

← Older revision		Revision as of 15:04, 5 November 2014
Line 53:		Line 53:
	There are several different ways that a new transition can be added to the current trace. The most important thing to remember is that each Trace object is completely immutable. This means that when you change a trace, you are actually getting a new Trace back. This means that when you carry out an animation step, you always have to make sure that you save the Trace object that is returned.		There are several different ways that a new transition can be added to the current trace. The most important thing to remember is that each Trace object is completely immutable. This means that when you change a trace, you are actually getting a new Trace back. This means that when you carry out an animation step, you always have to make sure that you save the Trace object that is returned.

	The simplest way to add a transition is to ~~add~~ it via ~~operation~~ id. For instance, if operation 0 is among the enabled operations for the current state, then		The simplest way to add a transition is to specify it with the name of the event to be executed and predicates to specify how the parameters for the event are to be allocated. Specifying no predicate will assume a predicate of "TRUE=TRUE" for the given event.

			<tt> t = t.execute("new","pp=PID1") </tt>

			If executing the event in a groovy environment (console or script), the event will be recognized as a method on the Trace class. This means that you can execute the event "new" as follows:

			<tt> t = t.new("pp=PID1") </tt>

			If you know the id that has been allocated by the ProB kernel to a given transition, this can be added via the "add" method. This will search the outgoing transitions from the current state and attempts to find one with a matching id. For instance, if operation 0 is among the enabled operations for the current state, then

	<tt> t = t.add(0) </tt>		<tt> t = t.add(0) </tt>
Line 59:		Line 67:
	will add operation 0 to the current trace, create a new trace, and return it.		will add operation 0 to the current trace, create a new trace, and return it.

	~~You~~ can also add operations via operation name and a list of the parameters. For instance		If you know the name and parameters combination for a specific transition, you can also add operations via operation name and a list of the parameters. For instance

	<tt> t = t.~~add~~("new",["PID3"]) </tt>		<tt> t = t.addTransitionWith("new",["PID3"]) </tt>

	will add the transition new(PID3) to the trace.		will add the transition new(PID3) to the trace.
Line 74:		Line 82:

	will execute any event with the name "name".		will execute any event with the name "name".

	~~Lastly, it is also possible to execute an event by treating it as if it were a method in the Trace class. For instance,~~

	~~<tt> t = t.new() </tt>~~

	~~will execute the event new (by default, the first solution for "new" is chosen). It is also possible to add a predicate as a parameter to filter for a particular solution. For instance,~~

	~~<tt> t = t.new("pp=PID1") </tt>~~

	~~will execute new(PID1) as long as pp is the name of the parameter for new.~~

	It also possible to move backwards and forwards within a trace.		It also possible to move backwards and forwards within a trace.

Joy Clark: /* Event B */

2014-11-05T14:56:37Z

Event B

← Older revision		Revision as of 14:56, 5 November 2014
Line 42:		Line 42:

	from the context menu that drops down.		from the context menu that drops down.

			You can also load Event B models into the API via the eventb_load command in the Api object. The eventb_load command accepts .bcm and .bcc files.

	== How to animate models ==		== How to animate models ==

Joy Clark: /* Open the ProB API from Source/JAR file */

2014-11-05T14:55:30Z

Open the ProB API from Source/JAR file

← Older revision		Revision as of 14:55, 5 November 2014
Line 23:		Line 23:
	In order to access the console from source or from a JAR file, start the application with the parameters -s (short for --shell) and -local (which specifies that you are running the application from a local computer). This will start a web server at a given port (the default is 8080, but it increments the port number if a port is already active). The shell can then be accessed at the following address:		In order to access the console from source or from a JAR file, start the application with the parameters -s (short for --shell) and -local (which specifies that you are running the application from a local computer). This will start a web server at a given port (the default is 8080, but it increments the port number if a port is already active). The shell can then be accessed at the following address:

	~~http://~~localhost:~~8080~~/sessions/GroovyConsoleSession		localhost:PORTNR/sessions/GroovyConsoleSession

	== How to load a model ==		== How to load a model ==

Joy Clark: /* How to open the Groovy Shell */

2014-11-05T14:54:23Z

How to open the Groovy Shell

← Older revision		Revision as of 14:54, 5 November 2014
Line 18:		Line 18:

	and hit <tt> ok</tt>.		and hit <tt> ok</tt>.

			== Open the ProB API from Source/JAR file ==

			In order to access the console from source or from a JAR file, start the application with the parameters -s (short for --shell) and -local (which specifies that you are running the application from a local computer). This will start a web server at a given port (the default is 8080, but it increments the port number if a port is already active). The shell can then be accessed at the following address:

			http://localhost:8080/sessions/GroovyConsoleSession

	== How to load a model ==		== How to load a model ==

Lukas Ladenberger at 14:39, 30 October 2014

2014-10-30T14:39:14Z

← Older revision		Revision as of 14:39, 30 October 2014
Line 1:		Line 1:
			[[Category:ProB Java API]]

	ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.		ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.


	== How to get started developing with ProB 2.0 ==		== How to get started developing with ProB 2.0 ==