SimB - Revision history

Michael Leuschel: /* Direct Activation */

2026-03-20T12:52:22Z

Direct Activation

← Older revision		Revision as of 12:52, 20 March 2026
Line 94:		Line 94:
	All other fields can be defined optionally.		All other fields can be defined optionally.

	* <tt>execute</tt> identifies the activated event by its name.		* <tt>execute</tt> identifies the activated event by its name. It can also be a list of events, in which case on of the events will be executed (see transitionSelection below)
	* <tt>after</tt> defines the scheduled time (in ms) when activating an event. By default, it is set to 0 ms, e.g., when this field is not defined explicitly.		* <tt>after</tt> defines the scheduled time (in ms) when activating an event. By default, it is set to 0 ms, e.g., when this field is not defined explicitly.
	* <tt>activating</tt> stores activations that will be scheduled when executing the event defined by <tt>execute</tt>. When the attribute is absent then no other activations are scheduled. The modeler can either write a String (to activate a single activation) or a list of Strings (to schedule multiple activations)		* <tt>activating</tt> stores activations that will be scheduled when executing the event defined by <tt>execute</tt>. When the attribute is absent then no other activations are scheduled. The modeler can either write a String (to activate a single activation) or a list of Strings (to schedule multiple activations)
Line 110:		Line 110:
	** <tt>uniform</tt> means that a transition is selected from all alternatives uniformly.		** <tt>uniform</tt> means that a transition is selected from all alternatives uniformly.
	* <tt>priority</tt> stores the priority for scheduling activations. Lower number means greater priority. Activations with same priorities and same scheduled time are processed in the order they are defined in the JSON file. Default value (if not defined) is 0.		* <tt>priority</tt> stores the priority for scheduling activations. Lower number means greater priority. Activations with same priorities and same scheduled time are processed in the order they are defined in the JSON file. Default value (if not defined) is 0.
			* <tt>activatingOnlyWhenExecuted</tt> is true by default, meaning that other activations will only be triggered if the <tt>execute</tt> was successful.
			* <tt>errorWhenNotExecuted</tt> is false by default. When set to true an error will be reported if <tt>execute</tt> was not successful.
	<pre>		<pre>
	{		{

Michael Leuschel: /* Using SimB */

2026-03-20T09:15:50Z

Using SimB

← Older revision		Revision as of 09:15, 20 March 2026
Line 49:		Line 49:
	Start SimB via "SimB" in the "Advanced" Menu after opening a machine.		Start SimB via "SimB" in the "Advanced" Menu after opening a machine.

	[[File:Open_SimB.png\|~~800px~~]]		[[File:Open_SimB.png\|600px]]

	Now, you can open a SimB file (JSON format) controlling the underlying formal model.		Now, you can open a SimB file (JSON format) controlling the underlying formal model.

	[[File:SimB_Window.png\|~~800px~~]]		[[File:SimB_Window.png\|600px]]

	As of version 1.16 of ProB you can also use SimB		As of version 1.16 of ProB you can also use SimB
Line 62:		Line 62:
	You can also open a SimB simulation dialog in the Animation menu of ProB Tcl/Tk.		You can also open a SimB simulation dialog in the Animation menu of ProB Tcl/Tk.
	Additional options are:		Additional options are:
	* -simb_profile to print out profiling information at the end of the simulation		* <tt>-simb_profile</tt> to print out profiling information at the end of the simulation
	* -simulate_until_ltl_ap LTLSTOP meaning that the simulation will stop when the LTL atomic property LTLSTOP is true.		* <tt>-simulate_until_ltl_ap LTLSTOP</tt> meaning that the simulation will stop when the LTL atomic property LTLSTOP is true.
	* -simulate_until_time TIME meaning that the simulation will stop when simulation time reaches or exceeds TIME		* <tt>-simulate_until_time TIME</tt> meaning that the simulation will stop when simulation time reaches or exceeds TIME

	A SimB file describes a list of SimB activations and SimB listeners to simulate the model.		A SimB file describes a list of SimB activations and SimB listeners to simulate the model.

Michael Leuschel: /* Using SimB */

2026-03-20T09:15:11Z

Using SimB

← Older revision		Revision as of 09:15, 20 March 2026
Line 61:		Line 61:
	** <tt>-mc-simulate SIMBFILE.json Reps Steps</tt> for Monte-Carlo simulation with Reps repetitions, each simulation the given number of steps		** <tt>-mc-simulate SIMBFILE.json Reps Steps</tt> for Monte-Carlo simulation with Reps repetitions, each simulation the given number of steps
	You can also open a SimB simulation dialog in the Animation menu of ProB Tcl/Tk.		You can also open a SimB simulation dialog in the Animation menu of ProB Tcl/Tk.
			Additional options are:
			* -simb_profile to print out profiling information at the end of the simulation
			* -simulate_until_ltl_ap LTLSTOP meaning that the simulation will stop when the LTL atomic property LTLSTOP is true.
			* -simulate_until_time TIME meaning that the simulation will stop when simulation time reaches or exceeds TIME

	A SimB file describes a list of SimB activations and SimB listeners to simulate the model.		A SimB file describes a list of SimB activations and SimB listeners to simulate the model.

Michael Leuschel: /* Interactive Elements in SimB */

2026-03-20T09:12:22Z

Interactive Elements in SimB

← Older revision		Revision as of 09:12, 20 March 2026
Line 157:		Line 157:
	== Interactive Elements in SimB ==		== Interactive Elements in SimB ==

	Interactive elements in SimB are ~~so called~~ SimB listeners.		Interactive elements in SimB are described by SimB listeners.
	A SimB listener consists of four fields <tt>id</tt>, <tt>event</tt>, <tt>predicate</tt>, and <tt>activating</tt>.		A SimB listener consists of four fields <tt>id</tt>, <tt>event</tt>, <tt>predicate</tt>, and <tt>activating</tt>.
	This means that the SimB listener associated with <tt>id</tt> listens on a manual/user interaction on <tt>event</tt> with <tt>predicate</tt> after which activations in <tt>activating</tt> are triggered.		This means that the SimB listener associated with <tt>id</tt> listens on a manual/user interaction on <tt>event</tt> with <tt>predicate</tt> after which activations in <tt>activating</tt> are triggered.

Michael Leuschel: /* Direct Activation */

2026-03-20T09:09:24Z

Direct Activation

← Older revision		Revision as of 09:09, 20 March 2026
Line 95:		Line 95:
	* <tt>activatingOnlyWhenExecuted</tt> stores a boolean flag which states whether activations in <tt>activating</tt> are only triggered when event in <tt>execute</tt> is triggered (or always)		* <tt>activatingOnlyWhenExecuted</tt> stores a boolean flag which states whether activations in <tt>activating</tt> are only triggered when event in <tt>execute</tt> is triggered (or always)
	* <tt>activationKind</tt> stores the kind of the activation. Possible options are <tt>multi</tt>, <tt>single</tt>, <tt>single:min</tt>, and <tt>single:max</tt>. The default value is <tt>multi</tt>.		* <tt>activationKind</tt> stores the kind of the activation. Possible options are <tt>multi</tt>, <tt>single</tt>, <tt>single:min</tt>, and <tt>single:max</tt>. The default value is <tt>multi</tt>.
	** <tt>multi</tt> means that the ~~activation will~~ be queued.		** <tt>multi</tt> means that multiple activations with the same id can be queued at the same time.
	** <tt>single</tt> means that ~~the~~ activation ~~will only~~ be queued ~~if there are no queued activations with~~ the same <tt>id</tt>		** <tt>single</tt> means that at most one activation with this id can be queued at the same time. Priority is given to activations triggered first. <tt>id</tt>
	** <tt>single:min</tt> means that ~~the~~ activation ~~will only~~ be queued ~~if (1) there are no queued activations for~~ the ~~same <tt>id</tt> or (2) there is a queued~~ activation with the ~~same <tt>id</tt> whose value for the scheduled time is greater. In the case of (2), the already queued activation will be discarded~~.		** <tt>single:min</tt> means that at most one activation with this id can be queued, retaining the activation with the minimal deadline.
	** <tt>single:max</tt> means that ~~the~~ activation ~~will only~~ be queued ~~if (1) there are no queued activations for~~ the ~~same <tt>id</tt> or (2) there is a queued~~ activation with the ~~same <tt>id</tt> whose value for the scheduled time is lower. In the case of (2), the already queued activation will be discarded~~.		** <tt>single:max</tt> means that at most one activation with this id can be queued, retaining the activation with the maximal deadline.
	* <tt>additionalGuards</tt> ~~stores optional~~ guards when executing the event stored in <tt>execute</tt>		* <tt>additionalGuards</tt> describes additional guards when executing the event stored in <tt>execute</tt>
	* <tt>fixedVariables</tt> ~~stores~~ a ~~Map~~. ~~Here, a variable (parameter~~, or non-~~deterministic assigned variable) is assigned to its value~~.		* <tt>fixedVariables</tt> is a map, mapping identifiers to values. The identifiers should be parameters of the executed event, or variables which are assigned non-deterministically by the event.
	* <tt>probabilisticVariables</tt>~~stores~~ a ~~Map~~. ~~Here a~~ variable (parameter, or non-deterministic assigned variable) is ~~assigned~~ to another ~~Map~~ defining the probabilistic ~~choice of~~ its value. The second Map ~~stores~~ Key-Value pairs where values are mapped to the probability/weight.		* <tt>probabilisticVariables</tt>is a map of maps. A variable (parameter, or non-deterministic assigned variable) is mapped to another map defining the probabilistic choices for its value. The second Map contains Key-Value pairs where values are mapped to the probability/weight.
	* <tt>transitionSelection</tt> determines how SimB choses from multiple possible transitions (due to not specified variables):		* <tt>transitionSelection</tt> determines how SimB choses from multiple possible transitions (due to not specified variables):
	** <tt>first</tt> (the default) means that the first transition is chosen for execution.		** <tt>first</tt> (the default) means that the first transition is chosen for execution.
	** <tt>uniform</tt> means that a transition is selected from all alternatives uniformly.		** <tt>uniform</tt> means that a transition is selected from all alternatives uniformly.
	* <tt>priority</tt> stores the priority for scheduling ~~<tt>execute</tt>~~. Lower number means greater priority. Activations with same priorities and same scheduled time are processed in the order they are defined in the JSON file. Default value (if not defined) is 0.		* <tt>priority</tt> stores the priority for scheduling activations. Lower number means greater priority. Activations with same priorities and same scheduled time are processed in the order they are defined in the JSON file. Default value (if not defined) is 0.

	<pre>		<pre>

Michael Leuschel: /* Probabilistic Choice */

2026-03-20T09:02:48Z

Probabilistic Choice

← Older revision		Revision as of 09:02, 20 March 2026
Line 125:		Line 125:
	=== Probabilistic Choice ===		=== Probabilistic Choice ===

	A probabilistic choice selects an ~~event~~ to be ~~executed in the future~~.		A probabilistic choice selects an activation to be triggered.
	It requires the two fields <tt>id</tt>, and <tt>chooseActivation</tt>. <tt>chooseActivation</tt> is a Map ~~storing~~ Key-Value pairs where activations (identified by their <tt>id</tt>) are mapped to a probability/weight~~. It is possible to chain multiple probabilistic choices together, but eventually, a direct activation must be reached~~.		It requires the two fields <tt>id</tt>, and <tt>chooseActivation</tt>. <tt>chooseActivation</tt> is a Map of Key-Value pairs where activations (identified by their <tt>id</tt>) are mapped to a probability/weight.
	The probabilities are always interpreted as weights and may sum to any number greater than zero.		The probabilities are always interpreted as weights and may sum to any number greater than zero.
	Thus, a <tt>probabilistic choice</tt> is of the following form:		Thus, a <tt>probabilistic choice</tt> is of the following form:

Michael Leuschel: /* Using SimB */

2026-03-20T09:00:53Z

Using SimB

← Older revision		Revision as of 09:00, 20 March 2026
Line 55:		Line 55:
	[[File:SimB_Window.png\|800px]]		[[File:SimB_Window.png\|800px]]

	As of version 1.16 you can also use SimB		As of version 1.16 of ProB you can also use SimB
	* within [[Using_the_Command-Line_Version_of_ProB\|probcli]] using the commands		* within [[Using_the_Command-Line_Version_of_ProB\|probcli]] using the commands
	** <tt>-simulate SIMBFILE.json Steps</tt> for running the simulation a certain number of steps		** <tt>-simulate SIMBFILE.json Steps</tt> for running the simulation a certain number of steps

Michael Leuschel: /* Using SimB */

2026-03-20T09:00:27Z

Using SimB

← Older revision		Revision as of 09:00, 20 March 2026
Line 55:		Line 55:
	[[File:SimB_Window.png\|800px]]		[[File:SimB_Window.png\|800px]]

	A SimB file ~~consists~~ of SimB activations and SimB listeners to simulate the model.		As of version 1.16 you can also use SimB
	SimB ~~activations encode~~ an ~~activation diagram with probabilistic~~ and ~~timing elements for automatic simulation.~~		* within [[Using_the_Command-Line_Version_of_ProB\|probcli]] using the commands
	~~To enable interactive simulation,~~ it is also ~~necessary to encode interactive elements aka. SimB listeners which~~ trigger other ~~SimB~~ activations.		** <tt>-simulate SIMBFILE.json Steps</tt> for running the simulation a certain number of steps
	~~Within these elements, the modeler~~ can user ~~B expressions which are evaluated on the current state~~.		** <tt>-rt_simulate SIMBFILE.json Steps</tt> for real-time simulation for a certain number of steps
			** <tt>-mc-simulate SIMBFILE.json Reps Steps</tt> for Monte-Carlo simulation with Reps repetitions, each simulation the given number of steps
			You can also open a SimB simulation dialog in the Animation menu of ProB Tcl/Tk.

			A SimB file describes a list of SimB activations and SimB listeners to simulate the model.
			A SimB activation controls the simulation: it can trigger an event in the formal model after a specified delay and it can also trigger other activations. Probabilistic annotations and B formulas can be used to influence the chosen event and the triggered activations.
			The SimB listeners enable interactive simulation: they can respond to user interaction by triggering SimB activations.

	The general structure of a SimB simulation is as follows:		The general structure of a SimB simulation is as follows:

Fabian Vu: /* Direct Activation */

2026-03-16T13:25:01Z

Direct Activation

← Older revision		Revision as of 13:25, 16 March 2026
Line 99:		Line 99:
	** <tt>first</tt> (the default) means that the first transition is chosen for execution.		** <tt>first</tt> (the default) means that the first transition is chosen for execution.
	** <tt>uniform</tt> means that a transition is selected from all alternatives uniformly.		** <tt>uniform</tt> means that a transition is selected from all alternatives uniformly.
	* <tt>priority</tt> stores the priority for scheduling <tt>execute</tt>. Lower number means greater priority. Activations with same priorities and same scheduled time are processed in the order they are defined in the JSON file. Default value is 0.		* <tt>priority</tt> stores the priority for scheduling <tt>execute</tt>. Lower number means greater priority. Activations with same priorities and same scheduled time are processed in the order they are defined in the JSON file. Default value (if not defined) is 0.

	<pre>		<pre>

Fabian Vu: /* Direct Activation */

2026-03-16T13:24:53Z

Direct Activation

← Older revision		Revision as of 13:24, 16 March 2026
Line 99:		Line 99:
	** <tt>first</tt> (the default) means that the first transition is chosen for execution.		** <tt>first</tt> (the default) means that the first transition is chosen for execution.
	** <tt>uniform</tt> means that a transition is selected from all alternatives uniformly.		** <tt>uniform</tt> means that a transition is selected from all alternatives uniformly.
	* <tt>priority</tt> stores the priority for scheduling <tt>execute</tt>. Lower number means greater priority. Activations with same priorities and same scheduled time are processed in the order they are defined in the JSON file.		* <tt>priority</tt> stores the priority for scheduling <tt>execute</tt>. Lower number means greater priority. Activations with same priorities and same scheduled time are processed in the order they are defined in the JSON file. Default value is 0.

	<pre>		<pre>