[SAL-HELP] Differences between sal-bmc and sal-inf-bmc

[Ambar Gadkari]

Skipped content of type multipart/alternative-------------- next part --------------
ex: CONTEXT =
BEGIN

mytype: TYPE = [0 .. 100];
mytype1: TYPE = [0 .. 10];

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
m1 : MODULE = 
BEGIN

INPUT	i1: mytype1	
INPUT   o2: mytype
OUTPUT	o1: mytype
LOCAL	cond1: BOOLEAN

INITIALIZATION
	cond1 = FALSE;
	o1 = 0      

TRANSITION
[
  TRUE --> 
	o1' = o1 + i1 + o2;
	cond1' = IF (o1' > 50) THEN TRUE ELSE FALSE ENDIF;
]
END;

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
m2 : MODULE = 
BEGIN

INPUT	i2: mytype1
INPUT   o1: mytype
OUTPUT	o2: mytype
LOCAL	cond2: BOOLEAN

INITIALIZATION
	cond2 = FALSE;
        o2 = 0
     
TRANSITION
[
  TRUE --> 
	o2' = o2 + 2*i2 - o1;
	cond2' = IF (o2' > 80) THEN TRUE ELSE FALSE ENDIF;
]
END;

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
sys : MODULE =
	m1 || m2;

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
th1: THEOREM m1|- G(NOT(cond1));
th2: THEOREM m2|- G(NOT(cond2));
th3: THEOREM sys|- G(NOT(cond1 AND cond2));
 
END