Some examples

From ClearSy Tools

1 Switch

Switch

Context

This system is a railway switch that has three sensors to measure its position. These sensors give the measures m1, m2, m3 that may be either normal, reverse or void.

The goal is to calculate the result "pos" indicating the switch position depending on the measures. Void measures should be disregarded. If two non void measures are contradictory then the result should be void. Otherwise, the result should be the position indicated by the non void measures, which then are consistent.

B models

The B specification of the component is:

  MACHINE switch1 
  SETS 
    POSITION = {normal,reverse,void} 
  OPERATIONS 
 	pos <-- measure(m1,m2,m3) = 
 	PRE 
 		m1 : POSITION & 
 		m2 : POSITION & 
 		m3 : POSITION 
 	THEN 
 		SELECT 
 			normal : {m1,m2,m3} & 
 			reverse /: {m1,m2,m3} 
 		THEN 
 			pos := normal 
 		WHEN reverse : {m1,m2,m3} & normal /: {m1,m2,m3} THEN 
 			pos := reverse 
 		ELSE 
 			pos := void 
 		END 
 	END 
  END

and its implementation is:

  IMPLEMENTATION 
  	switch1_i 
   
  REFINES 
  	switch1 
  	 
  OPERATIONS 
  	pos <-- measure(m1,m2,m3) =   
  	CASE m1 OF 
  		EITHER normal THEN 
  			IF m2  = reverse or m3 = reverse THEN 
  				pos := void 
  			ELSE 
  				pos := normal 
  			END 
  		OR reverse THEN 
  			IF m2 = normal or m3 = normal THEN 
  				pos := void 
  			ELSE 
  				pos := reverse 
  			END 
  		ELSE 
  			CASE m2 OF 
  				EITHER normal THEN 
  					IF m3 = reverse THEN 
  						pos := void 
  					ELSE 
  						pos := normal 
  					END 
  				OR reverse THEN 
  					IF m3 = normal THEN 
  						pos := void 
  					ELSE 
  						pos := reverse 
  					END 
  				ELSE 
  					pos := m3 
  				END 
  			END 
  		END 
  	END 
  END

This B project is completely proved with Atelier B ^[1].

COMPONENT	TC	POG	nPO	%Pr	B0C	C	Ada	C++	HIA
switch1	OK	OK	0	100	-
switch1_i	OK	OK	11	100	-	-	-	-	-
TOTAL	OK	OK	11	100	-	-	-	-	-

Code generated

ComenC generates two files: switch1.c and switch1.h.

 /******************************************************************************
 File Name               : switch1.c
 C Translator Version    : b2c V1.0 (08/08/2007)
 ******************************************************************************/
 /*--------------------------
  Added by the Translator
 --------------------------*/
 #include "b2c.h"
 #include "switch1.h"
 /*------------------------
  INITIALISATION Clause
 ------------------------*/
 void switch1__INITIALISATION(void) {
 }
 /*--------------------
 OPERATIONS Clause
 --------------------*/
 void switch1__measure(
  switch1__POSITION switch1__m1,
  switch1__POSITION switch1__m2,
  switch1__POSITION switch1__m3,
  switch1__POSITION *switch1__pos) {
  switch (switch1__m1) {
  case switch1__normal:
     if ((switch1__m2 ==
        switch1__reverse) ||
        (switch1__m3 ==
        switch1__reverse))
     {
        *switch1__pos = switch1__void;
     }
     else {
        *switch1__pos = switch1__normal;
     }
     break;
  case switch1__reverse:
     if ((switch1__m2 ==
        switch1__normal) ||
        (switch1__m3 ==
        switch1__normal))
     {
        *switch1__pos = switch1__void;
     }
     else {
        *switch1__pos = switch1__normal;
     }
     break;
  default:
     switch (switch1__m2) {
     case switch1__normal:
        if (switch1__m3 ==
           switch1__reverse)
        {
           *switch1__pos = switch1__void;
        }
        else {
           *switch1__pos = switch1__normal;
        }
        break;
     case switch1__reverse:
        if (switch1__m3 ==
           switch1__normal)
        {
           *switch1__pos = switch1__void;
        }
        else {
           *switch1__pos = switch1__reverse;
        }
        break;
     default:
        *switch1__pos = switch1__m3;
        break;
     }
     break;
  }
 }

 /******************************************************************************
 File Name               : switch1.h
 C Translator Version    : b2c V1.0 (08/08/2007)
 ******************************************************************************/
 #ifndef _switch1_h
 #define _switch1_h
 /*--------------------------
 Added by the Translator
 --------------------------*/
 #include "b2c.h"
 /*-------------------------------
  SETS Clause: enumerated sets
 -------------------------------*/
 typedef enum {
  switch1__normal,
  switch1__reverse,
  switch1__void
 } switch1__POSITION;
 /*------------------------
  INITIALISATION Clause
 ------------------------*/
 extern void switch1__INITIALISATION(void);
 /*--------------------
  OPERATIONS Clause
 --------------------*/
 extern void switch1__measure(
  switch1__POSITION switch1__m1,
  switch1__POSITION switch1__m2,
  switch1__POSITION switch1__m3,
  switch1__POSITION *switch1__pos);
 #endif

Retrieved from "http://tools.clearsy.com/index.php5?title=Some_examples"

Navigation