State-Machines and Code Generation - Revision history

imported>Andy: /* An Example */

2012-05-17T09:47:06Z

An Example

← Older revision		Revision as of 09:47, 17 May 2012
Line 40:		Line 40:
	end if;		end if;

	See the ~~complete~~ [http://wiki.event-b.org/images/Code.png ~~Ada Code~~]		See all of the Ada code that is generated [http://wiki.event-b.org/images/Code.png here].

imported>Andy at 09:45, 17 May 2012

2012-05-17T09:45:13Z

← Older revision		Revision as of 09:45, 17 May 2012
Line 40:		Line 40:
	end if;		end if;

	~~== Tooling ==~~		See the complete [http://wiki.event-b.org/images/Code.png Ada Code]

imported>Andy: /* An Example */

2012-05-17T09:37:09Z

An Example

← Older revision		Revision as of 09:37, 17 May 2012
Line 34:		Line 34:
	ac = when vv >= 100 then <''a2''> end		ac = when vv >= 100 then <''a2''> end

	The body can be viewed as a parallel composition of events, made up of all of the outgoing transitions of ''State A''. These events have disjoint and complete guards, so only one of the events will be enabled. The translation of the body gives rise to the following branching statement when ~~translating~~ to Ada,		The body can be viewed as a parallel composition of events, made up of all of the outgoing transitions of ''State A''. These events have disjoint and complete guards, so only one of the events will be enabled. The translation of the body gives rise to the following branching statement when translated to Ada,

	if vv < 100 then <''a1''>		if vv < 100 then <''a1''>

imported>Andy: /* An Example */

2012-05-17T09:20:05Z

An Example

← Older revision		Revision as of 09:20, 17 May 2012
Line 25:		Line 25:

	case sm_state is		case sm_state is
	when A => <body> ; sm_state := B;		when A => <''body''> ; sm_state := B;
	when B => <body> ; sm_state := A;		when B => <''body''> ; sm_state := A;
	...		...

	The <body> translation is determined, in part, by the number of outgoing transitions and the guards and actions of the elaborated events. When a state has a single outgoing transition, then the translation is straightforward. The event's action is mapped to a statement in the generated IL1 model. When a state has multiple outgoing transitions, then each outgoing transition of the state gives rise to a branching statement. Each outgoing transition is linked to an event, and the guards of the outgoing transitions must be disjoint and complete. Note that we do not yet generate proof obligations to show this. We illustrate the translation with an example fragment of the machine of Figure 1; the fragment refers to a variable vv: INT, and events ''ab'' and ''ac'', which elaborate the transitions in the diagram.		The <''body''> translation is determined, in part, by the number of outgoing transitions and the guards and actions of the elaborated events. When a state has a single outgoing transition, then the translation is straightforward. The event's action is mapped to a statement in the generated IL1 model. When a state has multiple outgoing transitions, then each outgoing transition of the state gives rise to a branching statement. Each outgoing transition is linked to an event, and the guards of the outgoing transitions must be disjoint and complete. Note that we do not yet generate proof obligations to show this. We illustrate the translation with an example fragment of the machine of Figure 1; the fragment refers to a variable ''vv: INT'', and events ''ab'' and ''ac'', which elaborate the transitions in the diagram.

	ab = when vv < 100 then <a1> end		ab = when vv < 100 then <''a1''> end
	ac = when vv >= 100 then <a2> end		ac = when vv >= 100 then <''a2''> end

	The body can be viewed as a parallel composition of events, made up of all of the outgoing transitions of ''State A''. These events have disjoint and complete guards, so only one of the events will be enabled. The translation of the body gives rise to the following branching statement when translating to Ada,		The body can be viewed as a parallel composition of events, made up of all of the outgoing transitions of ''State A''. These events have disjoint and complete guards, so only one of the events will be enabled. The translation of the body gives rise to the following branching statement when translating to Ada,

	if vv < 100 then <a1>		if vv < 100 then <''a1''>
	elsif vv >= 100 then <a2>		elsif vv >= 100 then <''a2''>
	end if;		end if;

	== Tooling ==		== Tooling ==

imported>Andy: /* An Example */

2012-05-17T09:18:10Z

An Example

← Older revision		Revision as of 09:18, 17 May 2012
Line 34:		Line 34:
	ac = when vv >= 100 then <a2> end		ac = when vv >= 100 then <a2> end

	The body ~~forms~~ a parallel composition of events, ~~with~~ disjoint and complete guards, ~~<ab \|\| ac>~~. ~~Then the~~ translation of the body, to a branching statement ~~results in the following~~ Ada ~~statement:~~		The body can be viewed as a parallel composition of events, made up of all of the outgoing transitions of ''State A''. These events have disjoint and complete guards, so only one of the events will be enabled. The translation of the body gives rise to the following branching statement when translating to Ada,

	if vv < 100 then <a1>		if vv < 100 then <a1>

imported>Andy: /* An Example */

2012-05-17T09:11:00Z

An Example

← Older revision		Revision as of 09:11, 17 May 2012
Line 29:		Line 29:
	...		...

	The <body> translation is determined, in part, by the number of outgoing transitions and the guards and actions of the elaborated events. When a state has a single outgoing transition, then the translation is straightforward. The event's action is mapped to a statement in the generated IL1 model. When a state has multiple outgoing transitions, then each outgoing transition of the state gives rise to a branching statement. Each outgoing transition is linked to an event, and the guards of the outgoing transitions must be disjoint and complete. Note that we do not yet generate proof obligations to show this. We illustrate the translation with an example~~, below. If we define~~ the ~~events, elaborating~~ the ~~transitions in the diagram, as follows: with~~ a ~~machine~~ variable vv:INT and events ''ab'' and ''ac'' ~~defined below~~,		The <body> translation is determined, in part, by the number of outgoing transitions and the guards and actions of the elaborated events. When a state has a single outgoing transition, then the translation is straightforward. The event's action is mapped to a statement in the generated IL1 model. When a state has multiple outgoing transitions, then each outgoing transition of the state gives rise to a branching statement. Each outgoing transition is linked to an event, and the guards of the outgoing transitions must be disjoint and complete. Note that we do not yet generate proof obligations to show this. We illustrate the translation with an example fragment of the machine of Figure 1; the fragment refers to a variable vv: INT, and events ''ab'' and ''ac'', which elaborate the transitions in the diagram.

	ab = when vv < 100 then <a1> end		ab = when vv < 100 then <a1> end

imported>Andy: /* An Example */

2012-05-17T09:04:38Z

An Example

← Older revision		Revision as of 09:04, 17 May 2012
Line 22:		Line 22:
	</div>		</div>

	We generate a subroutine that controls the state machine, and ~~code, in~~ the task body, to call the subroutines once in every execution cycle. Each state in the state machine is related to a case statement in the subroutine. For instance, the Ada code for the diagram in Figure 1 is,		We generate a subroutine that controls the state machine, and implements the actions. In the task body, we add a call the state-machine subroutines once in every execution cycle. Each state in the state machine is related to a case statement in the subroutine. For instance, the Ada code for the diagram in Figure 1 is,

	case sm_state is		case sm_state is

imported>Andy: /* An Example */

2012-05-17T09:02:53Z

An Example

← Older revision		Revision as of 09:02, 17 May 2012
Line 29:		Line 29:
	...		...

	The <body> translation is determined, in part, by the number of outgoing transitions and the guards and actions of the elaborated events. When a state has a single outgoing transition, then the translation is straightforward. The event's action is mapped to a statement in the generated IL1 model. When a state has multiple outgoing transitions, then each outgoing transition of the state gives rise to a branching statement. Each outgoing transition is linked to an event, and the guards of the outgoing transitions must be disjoint and complete. Note that we do not yet generate proof obligations to show this. We illustrate the translation with an example, below. If we define the events, elaborating the transitions in the diagram, as follows: with a machine variable v:INT and events ''ab'' and ''ac'' defined below,		The <body> translation is determined, in part, by the number of outgoing transitions and the guards and actions of the elaborated events. When a state has a single outgoing transition, then the translation is straightforward. The event's action is mapped to a statement in the generated IL1 model. When a state has multiple outgoing transitions, then each outgoing transition of the state gives rise to a branching statement. Each outgoing transition is linked to an event, and the guards of the outgoing transitions must be disjoint and complete. Note that we do not yet generate proof obligations to show this. We illustrate the translation with an example, below. If we define the events, elaborating the transitions in the diagram, as follows: with a machine variable vv:INT and events ''ab'' and ''ac'' defined below,

	ab = when v < 100 then <a1> end		ab = when vv < 100 then <a1> end
	ac = when v >= 100 then <a2> end		ac = when vv >= 100 then <a2> end

	~~Then the translation~~ of ~~the body~~ <ab \|\| ac> to a branching statement results in the following Ada statement:		The body forms a parallel composition of events, with disjoint and complete guards, <ab \|\| ac>. Then the translation of the body, to a branching statement results in the following Ada statement:

	if v < 100 then <a1>		if vv < 100 then <a1>
	elsif v >= 100 then <a2>		elsif vv >= 100 then <a2>
	end if;		end if;

	== Tooling ==		== Tooling ==

imported>Andy: /* An Example */

2012-05-17T08:53:33Z

An Example

← Older revision		Revision as of 08:53, 17 May 2012
Line 30:		Line 30:

	The <body> translation is determined, in part, by the number of outgoing transitions and the guards and actions of the elaborated events. When a state has a single outgoing transition, then the translation is straightforward. The event's action is mapped to a statement in the generated IL1 model. When a state has multiple outgoing transitions, then each outgoing transition of the state gives rise to a branching statement. Each outgoing transition is linked to an event, and the guards of the outgoing transitions must be disjoint and complete. Note that we do not yet generate proof obligations to show this. We illustrate the translation with an example, below. If we define the events, elaborating the transitions in the diagram, as follows: with a machine variable v:INT and events ''ab'' and ''ac'' defined below,		The <body> translation is determined, in part, by the number of outgoing transitions and the guards and actions of the elaborated events. When a state has a single outgoing transition, then the translation is straightforward. The event's action is mapped to a statement in the generated IL1 model. When a state has multiple outgoing transitions, then each outgoing transition of the state gives rise to a branching statement. Each outgoing transition is linked to an event, and the guards of the outgoing transitions must be disjoint and complete. Note that we do not yet generate proof obligations to show this. We illustrate the translation with an example, below. If we define the events, elaborating the transitions in the diagram, as follows: with a machine variable v:INT and events ''ab'' and ''ac'' defined below,

	~~body:~~

	ab = when v < 100 then <a1> end \|\|		ab = when v < 100 then <a1> end
	ac = when v >= 100 then <a2> end		ac = when v >= 100 then <a2> end

	Then ~~this is translated~~ to a branching statement~~, as~~ in ~~this example translation to~~ Ada:		Then the translation of the body <ab \|\| ac> to a branching statement results in the following Ada statement:

	if v < 100 then <a1>		if v < 100 then <a1>

imported>Andy: /* An Example */

2012-05-17T08:51:11Z

An Example

← Older revision		Revision as of 08:51, 17 May 2012
Line 31:		Line 31:
	The <body> translation is determined, in part, by the number of outgoing transitions and the guards and actions of the elaborated events. When a state has a single outgoing transition, then the translation is straightforward. The event's action is mapped to a statement in the generated IL1 model. When a state has multiple outgoing transitions, then each outgoing transition of the state gives rise to a branching statement. Each outgoing transition is linked to an event, and the guards of the outgoing transitions must be disjoint and complete. Note that we do not yet generate proof obligations to show this. We illustrate the translation with an example, below. If we define the events, elaborating the transitions in the diagram, as follows: with a machine variable v:INT and events ''ab'' and ''ac'' defined below,		The <body> translation is determined, in part, by the number of outgoing transitions and the guards and actions of the elaborated events. When a state has a single outgoing transition, then the translation is straightforward. The event's action is mapped to a statement in the generated IL1 model. When a state has multiple outgoing transitions, then each outgoing transition of the state gives rise to a branching statement. Each outgoing transition is linked to an event, and the guards of the outgoing transitions must be disjoint and complete. Note that we do not yet generate proof obligations to show this. We illustrate the translation with an example, below. If we define the events, elaborating the transitions in the diagram, as follows: with a machine variable v:INT and events ''ab'' and ''ac'' defined below,

	ab = when v < 100 then <a1> end;		body:

			ab = when v < 100 then <a1> end \|\|
	ac = when v >= 100 then <a2> end		ac = when v >= 100 then <a2> end

	Then this is translated to a branching statement, as in this example translation to Ada:		Then this is translated to a branching statement, as in this example translation to Ada:

	if v < 100 then <a1>		if v < 100 then <a1>
	elsif v >= 100 then <a2>		elsif v >= 100 then <a2>