[SAL-HELP] strange counter-example from sal-smc

[Graeme Smith]

Hi,

When I try to check the attached SAL file with sal-smc, I get the 
attached counter-example. Why does the skip transition happen when the 
cop transition is obviously enabled?

Graeme
-------------- next part --------------
increment: CONTEXT = 
BEGIN

	NAT: TYPE = [0..10];
	EVENT: TYPE = {Init, AOp, COp, skip};

	main: MODULE = 
	BEGIN
	  LOCAL s,t : NAT
	  LOCAL ev: EVENT
          INITIALIZATION [s=t 
				--> s IN {n:NAT|true}; 
				    t IN {n:NAT|true}; 
				    ev =Init]
	  TRANSITION
		[opa:  ev=Init AND (s'=s+1 OR s'=s+2) AND ev'=AOp 
				--> s' IN {n:NAT|true}; 
				    ev' =AOp
		[]
		opc: ev=AOp AND t'=t+1 AND ev'=COp 
				--> t' IN {n:NAT|true}; 
				    ev' =COp
		[]
		skip: ELSE  --> ev'=skip
		]
		END;


refine: THEOREM main |-  X(ev=skip OR (ev=AOp AND X(ev=COp)));

END









-------------- next part --------------
Counterexample:
========================
Path
========================
Step 0:
--- System Variables (assignments) ---
ba-pc!1 = 4
s = 6
t = 6
ev = Init
------------------------
Transition Information: 
(module instance at [Context: increment, line(29), column(16)]
  (label opa
    transition at [Context: increment, line(16), column(11)]))
------------------------
Step 1:
--- System Variables (assignments) ---
ba-pc!1 = 1
s = 7
t = 6
ev = AOp
------------------------
Transition Information: 
(module instance at [Context: increment, line(29), column(16)]
  (label skip
    else transition at [Context: increment, line(24), column(10)]))
------------------------
Step 2:
--- System Variables (assignments) ---
ba-pc!1 = 0
s = 7
t = 6
ev = skip
------------------------
Transition Information: 
(module instance at [Context: increment, line(29), column(16)]
  (label skip
    else transition at [Context: increment, line(24), column(10)]))
------------------------
Step 3:
--- System Variables (assignments) ---
ba-pc!1 = 2
s = 7
t = 6
ev = skip