var HH2O, DH2O, HCH4, ALARM, PUMPON ;

const delta = 2, w = 12, epsilon=5 , zeta= 20, kappa=2 ;
	-- delta   response time of PUMP and ALARMS after trigger
	-- epsilon time taken by pump to bring water level to below HH2O
	-- w       time taken for water level to be dangerous after high
	-- zeta	   minimum separation between two methane leaks. 
	-- kappa   maximum duration of methane leak.
-- correctness under 2*(epsilon + delta) + kappa < w < zeta
-- there is no dangerous water level.

-- Alarm control
-------------------------------------------------------------
define alarm1 as  
!(<>(  ( [DH2O] && 
                   ( (tlen >= delta) &&
                   	 (true ^ ([!(ALARM)] ||  < !(ALARM) > )
 )  )  )           ) )
;
------------------------------------------------------------
define alarm2 as
!(<>(  ( [HCH4] && 
                   ( (tlen >= delta) &&
                   	 (true ^ ([!(ALARM)] ||  < !(ALARM) > )
 )  )  )           ) )
;
-------------------------------------------------------------
define alarm3 as
!(<>(  ( [!HCH4 && !DH2O] && 
                   ( (tlen >= delta) &&
                   	 (true ^ ([ALARM] ||  < ALARM > )
 )  )  )           ) )
;
--------------------------------------------------------------
-- Water seepage Assumptions
define water1 as 
   [] ( [[ DH2O => HH2O ]] ) ;

define water2 as
 !(<>(  < (!(-HH2O) ) > ^ (   [[HH2O]] &&
                               (   (tlen < w)  ^  < DH2O >  )
  )  )	 			  )                    
;
--------------------------------------------------------------
-- Pump control
define pump1 as
!(<>(  ( [HH2O && !HCH4] && 
                   ( (tlen >= delta) &&
                   	 (true ^ ([!(PUMPON)] ||  < !(PUMPON) > )
 )  )  )           ) )
;
---------------------------------------------------------------
define pump2 as
!(<>(  ( [!HH2O || HCH4] && 
                   ( (tlen >= delta) &&
                   	 (true ^ ( [PUMPON] ||  < PUMPON > )
  )  )  )          ) )
;
---------------------------------------------------------------
-- Pump capacity assumption
define pumpcap1 as
!(<>(  ( [PUMPON] && 
                   ( (tlen >= epsilon) &&
                   	 (true ^ ([HH2O] ||  < HH2O > )
 )  )  )           ) )
;
------------------------------------------------------------------
--  Methane Release assumptions
define methane1 as
   [] ( <!-!HCH4>^[!HCH4]^<HCH4> => tlen >= zeta ) ;
  
define methane2 as
   [] ( [HCH4] => tlen <= kappa ) ;
  
infer
( alarm1 && alarm2 && alarm3 && water1 && water2 && pump1 
  && pump2 && pumpcap1 && methane1 && methane2
) => sdur DH2O = 0 
.