-- The lift controller from
-- Dines Bjorner, Trusted Computing Systems in Proc ICSE14, Melbourne, 
-- Australia

--   Floors are numbered 0,1, ... , 4
--      Current version of dcvalid does not allow formulae parameterised by
--	floor number i. We must repeat the formulae for each value of i. 

var   flooris0, flooris1,flooris2, flooris3, flooris4,
	dooris0, dooris1, dooris2, dooris3, dooris4,
	doorcls,
	callhas0, callhas1, callhas2, callhas3, callhas4,
	sendhas0, sendhas1, sendhas2, sendhas3, sendhas4,
	moveis0, moveis1, moveis2, moveis3, moveis4,
	moveisidle;
		
const ts=90, to=3, tmax=5, tm=10 ;
--  It is assumed that ts > (n+1)*(tmax + tm) and to <= tmax
 
-- data invariants

define prop1 as
[[ !(	flooris0&&flooris1 || flooris0&&flooris2 || flooris0&&flooris3 || flooris0&&flooris4 || 
	flooris1&&flooris2 || flooris1&&flooris3 || flooris1&&flooris4 ||
	flooris2&&flooris3 || flooris2&&flooris4 || flooris3&&flooris4
    )
  && (flooris0 || flooris1 || flooris2 || flooris3 || flooris4)
]]
;

define prop2 as
[[ !(	dooris0&&dooris1 || dooris0&&dooris2 || dooris0&&dooris3 || dooris0&&dooris4 || dooris0&&doorcls ||
	dooris1&&dooris2 || dooris1&&dooris3 || dooris1&&dooris4 || dooris1&&doorcls ||
	dooris2&&dooris3 || dooris2&&dooris4 || dooris2&&doorcls ||
        dooris3&&dooris4  || dooris3&&doorcls || dooris4 && doorcls
    )
 && (dooris0 || dooris1 || dooris2 || dooris3 || dooris4 || doorcls)
]]
;


define prop3 as
[[ !(	moveis0&&moveis1 || moveis0&&moveis2 || moveis0&&moveis3 || moveis0&&moveis4 || moveis0&&moveisidle ||
	moveis1&&moveis2 || moveis1&&moveis3 || moveis1&&moveis4 || moveis1&&moveisidle ||
	moveis2&&moveis3 || moveis2&&moveis4 || moveis2&&moveisidle ||
        moveis3&&moveis4  || moveis3&&moveisidle || moveis4 && moveisidle
    )
 && (moveis0 || moveis1 || moveis2 || moveis3 || moveis4 || moveisidle)
]]
;


-- Initial conditions

define prop4 as
< moveisidle && flooris0 && dooris0 && 
  !sendhas0 && !sendhas1 && !sendhas2 && !sendhas3 && !sendhas4 &&
  !callhas0 && !callhas1 && !callhas2 && !callhas3 && !callhas4 
>^ true
;

-- up behaviour

define prop5 as
({moveisidle && flooris0} -> {moveis1})
&&
({moveisidle && flooris1} -> {moveis2})
&&
({moveisidle && flooris2} -> {moveis3})
&&
({moveisidle && flooris3} -> {moveis4})
;

-- down behaviour
define prop6 as
({moveisidle && flooris4} -> {moveis0})
;

-- stop behaviour
define prop7a as
({moveis0} -> {moveisidle && flooris0}) ;

define prop7b as
({moveis1} -> {moveisidle && flooris1}) ;

define prop7c as
({moveis2} -> {moveisidle && flooris2}) ;

define prop7d as
({moveis3} -> {moveisidle && flooris3}) ;

define prop7e as
({moveis4} -> {moveisidle && flooris4})  ;

-- door behaviour
define prop8 as
[[
moveisidle && flooris0 => dooris0
]]
&&
[[
moveisidle && flooris1 => dooris1
]]
&&
[[
moveisidle && flooris2 => dooris2
]]
&&
[[
moveisidle && flooris3 => dooris3
]]
&&
[[
moveisidle && flooris4 => dooris4
]]
;

define prop9 as
[[!moveisidle => doorcls ]]
;

-- send behaviour
define prop10 as
[[ dooris0 => !sendhas0 ]]
&&
[[ dooris1 => !sendhas1 ]]
&&
[[ dooris2 => !sendhas2 ]]
&&
[[ dooris3 => !sendhas3 ]]
&&
[[ dooris4 => !sendhas4 ]]
;

-- call behaviour
define prop11 as
[[ dooris0 => !callhas0 ]]
&&
[[ dooris1 => !callhas1 ]]
&&
[[ dooris2 => !callhas2 ]]
&&
[[ dooris3 => !callhas3 ]]
&&
[[ dooris4 => !callhas4 ]]
;

-- timing
-- Minopentime
define prop12 as
[] ([!dooris0]^[dooris0]^[!dooris0] => slen=2^ slen >= to )
&&
[] ([!dooris1]^[dooris1]^[!dooris1] => slen=2^ slen >= to )
&&
[] ([!dooris2]^[dooris2]^[!dooris2] => slen=2^ slen >= to )
&&
[] ([!dooris3]^[dooris3]^[!dooris3] => slen=2^ slen >= to )
&&
[] ([!dooris4]^[dooris4]^[!dooris4] => slen=2^ slen >= to )
;

define prop13 as
[] ([[!moveisidle]] => slen <= tm )
;

-- assumption 
define prop14 as
[] ( [dooris0] => (slen <= tmax) )
&&
[] ( [dooris1] => (slen <= tmax) )
&&
[] ( [dooris2] => (slen <= tmax) )
&&
[] ( [dooris3] => (slen <= tmax) )
&&
[] ( [dooris4] => (slen <= tmax) )
;

define concl1 as
[[ (dooris0 => flooris0) &&
   (dooris1 => flooris1) &&
   (dooris2 => flooris2) &&
   (dooris3 => flooris3) &&
   (dooris4 => flooris4)
]]
;


define concl2 as
[] (slen <= ts || slen <=ts^[dooris0]^true)
;

define concl3 as
[] ([!dooris3]^[dooris3]^[!dooris3]  => slen >= to)
;

infer
(
       prop1 
    && prop2 
    && prop3 
    && prop4 
    && prop5
    && prop6 
    && prop8 
    && prop9 
--    && prop10 
--    && prop11 
    && prop12 
    && prop13 
   && prop14
   && prop7a
   && prop7b
   && prop7c
   && prop7d
   && prop7e
)
=> concl1 && concl2 && concl3
.