BLESS behavior for threads and devices is expressed as state-transition machines. A set of states is declared, followed by transitions from a source state to a destination state when a transition condition is true, with possibly an action performed after leaving the source state and prior to entering the destination state.
There are four kinds of states. There must be exactly one “initial” state which cannot be the destination of any transition. There may be one or more “final” states which cannot be the source of any transition. Entering a “complete” state suspends execution until next dispatch. An “execution” state is transitory between dispatch and suspension, therefore must always have at least one, enabled outgoing transition .
The code below shows a simple, but non-trivial thread behavior in BLESS. (It can be found in iPCA_Operation_Threads.aadl in the Open_PCA project in the Open PCA Pump example.)
thread Patient_Bolus_Checker
features
minimum_time_between_bolus: in data port Physical_Types::Minute
{BLESS::Assertion => "<<:=MINIMUM_TIME_BETWEEN_BOLUS>>";};
patient_button_request: in event port
{BLESS::Assertion => "<<PATIENT_BUTTON_REQUEST>>";};
patient_request_not_too_soon: out event port
{BLESS::Assertion => "<<PATIENT_REQUEST_NOT_TOO_SOON(now)>>";};
patient_request_too_soon: out event port
{BLESS::Assertion => "<<PATIENT_REQUEST_TOO_SOON(now)>>";};
stop: in event port; --use lower case 'stop'
properties
Dispatch_Protocol => Sporadic;
end Patient_Bolus_Checker;
thread implementation Patient_Bolus_Checker.i
annex BLESS
{**
assert
<< LPB: :PATIENT_REQUEST_NOT_TOO_SOON(LAST_PATIENT_BOLUS) and
not (exists t~time in LAST_PATIENT_BOLUS,,now
that PATIENT_REQUEST_NOT_TOO_SOON(t)) >>
invariant << LPB() >>
variables
last_patient_bolus ~ time:=0 s
-- variable last_patient_bolus holds ghost value LAST_PATIENT_BOLUS
<< AXIOM_LPB: : last_patient_bolus = LAST_PATIENT_BOLUS >>;
states
start: initial state
<< last_patient_bolus = 0 ms and now=0 and LPB() >>;
run: complete state
<< LPB()>>;
check_last_bolus_time: state
<< LPB() and PATIENT_BUTTON_REQUEST@now and AXIOM_LPB() >>;
done: final state;
transitions
go: start-[ ]-> run{};
button: run -[on dispatch patient_button_request]-> check_last_bolus_time{};
nottoosoon: check_last_bolus_time -[
(now-minimum_time_between_bolus?) > last_patient_bolus
]-> run
{ << LPB() and PATIENT_BUTTON_REQUEST@now and AXIOM_LPB() and
(now-MINIMUM_TIME_BETWEEN_BOLUS) > last_patient_bolus >>
patient_request_not_too_soon!
; << PATIENT_REQUEST_NOT_TOO_SOON(now) >>
last_patient_bolus:=now
<< PATIENT_REQUEST_NOT_TOO_SOON(now) and last_patient_bolus=now
and AXIOM_LPB() >>};
toosoon: check_last_bolus_time -[
(now-minimum_time_between_bolus?) <= last_patient_bolus
]-> run
{ patient_request_too_soon! };
quit: run-[on dispatch stop]->done{};
**};
end Patient_Bolus_Checker.i;