program AltitudeController

var 


int cWakeupDOI, domain 0 .. 1; 
int mAltBelow, domain 0 .. 1;
int mDOIStatus, domain 0 .. 1;
int mInit, domain 0 .. 1;
int mInhibit, domain 0 .. 1;
int mReset, domain 0 .. 1;

int mAltFail, domain 0 .. 1;

int mInitLessThanInitDur, domain 0 .. 1;  	//  Models the failure of condition (mcStatus == init)										//  being true more than 0.6 sec.
 
int mAltFailLessThanFaultDur, domain 0 .. 1;	//  Models the failure of condition (mAltimeterFail == true)
						//  being true more than 2 sec.

int mAwaitLessThanFaultDur, domain 0 .. 1;	//  Models the failure of condition (mcStatus == awaitDOIon)
						//  being true more than 2 sec.


int mcStatus = -1, domain -1 .. 2; 		//  (mcStatus == -1)  <---> init
						//  (mcStatus == 0)   <---> awaitDOIon
						//  (mcStatus == 1)   <---> standby
						//  (mcStatus == 2)   <---> fault



process  Controller

begin

((mcStatus == -1) && (mInit == 1)) ->  mcStatus = 1; mInit = 0;

|

((mcStatus == 1) && (mReset == 0)) -> mcStatus = -1; mReset = 1;

|

((mcStatus == 1) && (mAltBelow == 0) && (mInhibit == 0) && (mDOIStatus == 0)) -> mcStatus = 0; mAltBelow = 1;

|

((mcStatus == 0) && (mDOIStatus == 0)) -> mcStatus = 1; mDOIStatus = 1;

|

((mcStatus == 0) && (mReset == 0)) -> mcStatus = -1; mReset = 1;




read 
mAltBelow, mDOIStatus, mInit, mInhibit, mReset, mAltFail,
mInitLessThanInitDur, mAltFailLessThanFaultDur, mAwaitLessThanFaultDur, mcStatus; 

 
write 
cWakeupDOI, mAltBelow, mDOIStatus, mInit, mInhibit, mReset,  mcStatus; 


end








fault Malfunction

begin

(mInitLessThanInitDur == 1 ) -> mInitLessThanInitDur = 0; mcStatus = 2;

|

(mAltFailLessThanFaultDur == 1 ) -> mAltFailLessThanFaultDur = 0; mcStatus = 2;

|

( mAwaitLessThanFaultDur == 1 ) -> mAwaitLessThanFaultDur = 0; mcStatus = 2;



end



invariant


((mcStatus == -1) || (mcStatus == 0) || (mcStatus == 1))



specification




destination

((mAltFails == 1) && ( mcStatuss == 1) && ( mcStatusd == 0)) ||
           ( mcStatuss == 2) && (( mcStatusd == 1) || ( mcStatusd == 0))
||
           (( mcStatuss == 2) && (mResets == 1))


noRelation



init

state

cWakeupDOI = 0; 
mAltBelow = 1;
mDOIStatus = 0;
mInit = 1;
mInhibit = 0;
mReset = 0;

mAltFail = 0;

mInitLessThanInitDur = 1;
mAltFailLessThanFaultDur = 1;
mAwaitLessThanFaultDur = 1;


mcStatus = -1;