-- Example for statechart compiler: burglar alarm controller
-- Intended to correspond with the graphical statechart
-- examples.

include "statechartcompiler.csp"

-- The alarm is constructed of two nearly independent parallel
-- processes: one isthe number pad that determines (subject to things
-- like timeout and too many attempts as limitations) when the
-- last D digits input are the code number for arming and disarming
-- the alarm.  This appears in pad.csp and padcomps.csp as really
-- quite a subtle process.  It indicates to the main controller
-- (the subject of this file) when this has been done, and the controller
-- moves around a collection of states according to this signal and
-- alarm signals (plus timeouts).

--***********************************************************************

-- DEFINITIONS OF VARIABLES, LABELS ETC.

-- We need to define the following types which contain the names of identifiers,
-- action labels, and names for sequential graphs. 

Pad_Digits = 4  -- user definable number of digits in code

digits = {0..Pad_Digits-1}

digit_range = {0..1}  --  range of key pad: usually {0..9} of
                      -- course, but data independence would
                      -- suggest that for verification purposes
                      -- smaller ranges...perhaps {0..1} would do.

datatype Identifiers = en.{0..Pad_Digits} |  d.digit_range |
                       key | press | 
                       alarm | lighton |
                       siren | go |
                       kc | key_limit |
                       EW_Time | Idle_Time | Leave_Time| Return_Time |
                       lastdigs
                       

datatype ActLabel =  error | progress  -- compulsory
                     | spec_error  -- for Spec
                     | kc_ew
                     | kc_pa


datatype SGlabel = Digit.digits
                   | Mainpad
                   | Key_Man
                   | KC
                   | Controller
                   | Whole_Alarm
                   | Box
                   | Spec_label

alarm_zones = {0..3}  -- zones where an alarm signal might come from
                      -- here {0,1,2,3} certainly OK by DI.
                      -- (constants 0,1 + 2 others)

Inputs = union({(key,0,digit_range),(press,0,nbool)}, -- user inputs
               {(alarm,0,alarm_zones)})   -- the burglar's inputs!     
          
Variables = {(lighton,0,alarm_zones),
             (en.j,0,nbool),
             (go,0,nbool),
             (kc,0,{0..CV(key_limit)+1}),
             (siren,0,nbool), 
             (lastdigs,<>,prefixes) | j <- {0..Pad_Digits}}

SigChans = {}

prefixes={<CV(d.i) | i <- <0..j-1>> | j <- {0..Pad_Digits}}

Outputs = {siren,lighton}  
     -- must be a subset of identifiers used in the two above

Constants = union({(d.i,i%2)| i <- {0..Pad_Digits-1}},
            {(EW_Time,1),(Idle_Time,1), (Leave_Time,1),(Return_Time,Pad_Digits+1),(key_limit,12)})  
                        -- timer limits for nondet, Return is bigger
                        -- because we want it to be possible to turn
                        -- alarm off!

--*******************************************************************

-- DEFINITION OF GRAPH
             

Controller_sg =
 let
  State_0 = (0,<(TRUE,progress,
                 <(go,FALSE),
                  (siren,FALSE),
                  (lighton,ZERO)>,1)>,
             <>)

  Disarmed_1 = (1,<(Ival(go),progress,<(go,FALSE)>,2)>,
             <>)

  Leaving_2 = (2,<(Ival(go),progress,<(go,FALSE)>,1),
                  (andf(notf(Ival(go)),
                        timer(En.(Controller,2),Ival(Leave_Time))),
                   progress, <>,3)>,
              <>)

  Armed_3 = (3,<(Ival(go),progress,<(go,FALSE)>,1),
                (andf(notf(Ival(go)),
                      gt(Ival(alarm),ONE)),
                 progress,
                 <(siren,TRUE),(lighton,Ival(alarm))>,4),
                (andf(notf(Ival(go)),
                      eqf(Ival(alarm),ONE)),
                 progress,
                 <(lighton,Ival(alarm))>,6)
               >,
              <>)

  Alarmed_4 = (4,<(Ival(go),progress,<(go,FALSE),(siren,FALSE)>,5)>,
              <>)

  Report_5 = (5,<(Ival(go),progress,<(go,FALSE),(lighton,ZERO)>,1)>,
              <>)

  Returning_6 = (6,<(Ival(go),progress,<(go,FALSE)>,1),
                  (andf(notf(Ival(go)),
                        timer(En.(Controller,6),Ival(Return_Time))),
                   progress, <(siren,TRUE)>,4)>,
                  <>)

within {State_0,Disarmed_1,Leaving_2,Armed_3,Alarmed_4,Report_5,Returning_6}

Controller_g = (Controller_sg,Controller,0,{go})

--************************************************************************

-- Collecting information together for whole system (in part from
-- the included files)
               
Named_Timers_Lim = {}
ND_NT = {}

Timed_Nodes_Lim = {((Controller,2),CV(Leave_Time)),
                   ((Controller,6),CV(Return_Time)),
                   ((KC,1),CV(Idle_Time)),
                   ((Mainpad,2),CV(EW_Time))}

ND_TN = Timed_Nodes

AllCharts = {Spec_g,
             Box_g(Box),  -- a null statechart with a single state 0
             kc_g,
             KeyMan,Digit_g(i),Mainpad_g, Controller_g | i <- digits}

Burglar_Alarm_sc = SCTree.Box.{}.{(0,Pad_sc),(0,lift(Controller))}


indstates = {(KC,1)}  -- a set of states to check for reachability
                        -- MUST BE DEFINED, even if empty

--  Standard checks.... 

assert Time_Error_Spec [FD= Time_Error_Imp(Burglar_Alarm_sc)  

-- tests for all types of run-time errors, plus race conditions,
-- as well as checking for deadlock faults in the compiler (we think
-- that any deadlock not preceded by an error event is almost
-- certainly a compiler error).

assert STOP [T= SYSTEM(Burglar_Alarm_sc)\diff(Events,{|isat|})  

-- Tests for reachability of members of indstates.  Note that checks
-- like this do not behave ideally with attempts to prove things
-- about a chart under nondeterministic parameters, since such a check
-- will simply demonstrate that it is sometimes possible to reach the
-- state, not that it is for all values of the parameter.

--************************************************************************

-- A watchdog statechart

-- This is a statechart which is run in parallel with an implementation
-- and can read its variables.  It may not, however, write to any
-- variable used by the implementation.  Its function is to keep track
-- (as it wishes) of what goes on and to raise a flag (spec_error) which
-- can be caught by the Time and Error check if the implementation does
-- something wrong.  These conditions mean that it never interferes with
-- the implementation.

-- The one here is going to ensure that the siren never goes off until
-- firstly the code number has been typed in and secondly an alarm
-- signal has appeared.

-- We will keep track of the most recent digits more abstractly than
-- in the implementation of the pad: 

-- prefixes (see above) is the set of all prefixes of the target string,
-- so the following function (in the style of curried functions of state
-- used in the compiler) calculates the longest final subsequence of
-- xs^<x> which is a prefix of the target.  This is the longest potentially
-- interesting sequence of previous digits.

snocf(x,xs)(S) =
    let
     (v0,n0) = x(S)
     (v1,n1) = xs(S)
     newv = greatest_suffix(v1^<v0>,prefixes)
    within
     (newv,n1^n0)

greatest_suffix(xs,S) = head(<ys | ys <- tails(xs), member(ys,S)>)

tails(<>) = <<>>
tails(xs) = <xs>^tails(tail(xs))

-- The specification moves from State0 to State1 when the digits have
-- been correctly entered, and prior to that does the calculations to
-- know when this has been done.  It moves from State1 to State2 when
-- alarm is not 0, and only then does it not raise an alarm when the
-- siren does off.

Spec_sg = let
            State0 = (0,<(Ival(siren),spec_error,<>,2),
                         (andf(ch(press),Ival(press)),
                             progress,
                             <(lastdigs,snocf(Ival(key),Ival(lastdigs)))>,0),
                         (eqf(Ival(lastdigs),K(<CV(d.i) | i <- <0..3>>)),
                             progress,<>, 1)>,<>)

            State1 = (1,<(Ival(siren),error,<>,2),
                         (notf(eqf(Ival(alarm),K(0))),progress,<>,2)>,
                        <>)

            State2 = (2,<>,<>)

           within {State0,State1,State2}

Spec_g = (Spec_sg,Spec_label,0,{})

SysAndSpec_sc = SCTree.Box.{}.{(0,Burglar_Alarm_sc),(0,lift(Spec_label))}

assert STOP [T= SYSTEM(SysAndSpec_sc)\diff(Events,{action.spec_error})  

--***********************************************************************

-- A CSP-style specification

-- We can specify our burglar alarm directly in terms of the
-- events communicated by the CSP implementation.  This particular
-- model is not that good for this type of specification since the
-- event of typing in a code number is rather diffuse (and almost
-- certainly better handled using the watchdog style above).  The
-- following specification asserts that the siren cannot sound for
-- at least k time units from the start:

SirenWait(0) = outp.(siren,1) -> SirenWait(0)
               [] tock -> SirenWait(0)

SirenWait(k) = tock -> SirenWait(k-1)

-- We can check this for various values via the trace check: we believe that
-- the following are the (parameterised) limit.

assert SirenWait(CV(Leave_Time)+Pad_Digits+1) [T=
       SYSTEM(Burglar_Alarm_sc)\diff(Events,{tock,outp.(siren,1)})

assert SirenWait(CV(Leave_Time)+Pad_Digits+2) [T=
       SYSTEM(Burglar_Alarm_sc)\diff(Events,{tock,outp.(siren,1)})

--***********************************************************************

-- burglar alarm's keypad

kc_sg =
  let
    State0 = (0,<(TRUE,progress,
             <(kc,ZERO)>,1)
                >,<>)

    State1 = (1,<(andl(<ch(press),Ival(press),eqf(Ival(kc),Ival(key_limit))>), 
                 kc_ew,
                 <>,OMEGA),
                 (andl(<ch(press),Ival(press),gt(Ival(key_limit),Ival(kc))>),
                 progress,
                 <(kc,succ(Ival(kc)))>,1),
                 (andf(notf(Ival(press)),timer(En.(KC,1),Ival(Idle_Time))),kc_pa,<>,OMEGA)
                 >,
                 <>)
within {State0,State1}

kc_g = (kc_sg,KC,0,{kc,press})

sg_mainpad = 
 let
   inactive0 = (0,<(andf(ch(press),Ival(press)), progress,
                 <(en.0,TRUE)>,1)>,
                 <>)

   active1 = (1,<(Ival(en.Pad_Digits),progress,<(go,TRUE),(en.Pad_Digits,FALSE)>,0)>,
                <(kc_ew,2),
                 (kc_pa,0)>)

   error_wait2 = (2,<(timer(En.(Mainpad,2),Ival(EW_Time)),progress,<>,0)>,
                 <>)

within {inactive0, active1, error_wait2}

Mainpad_g = (sg_mainpad,Mainpad,0,{})


mainpad_sc = SCTree.Mainpad.{kc_ew,kc_pa}.
             union({(1,lift(Digit.i)) | i <- digits}, {(1,lift(KC))})

Pad_sc = SCTree.Box.{}.{(0,mainpad_sc),(0,lift(Key_Man))}

--***********************************************************************

-- components for the burglar alarm's keypad

-- The digit processes below act as a chain, each enabling the
-- next when it is itself enabled and its digit is entered.

-- The enablement signal from the last digit becomes the signal
-- that the code has been correctly entered.

-- The odd initialisation is explained by the fact that these
-- processes are woken up through the pad_active state (the one
-- they run within) being entered through a digit being pressed,
-- which in turn has to be allowed for.

sg_digit(i) =
  let
    State0 = (0,<(TRUE,progress,
             <(en.(i+1),andf(K(bmap(i==0)),eqf(Ival(key),Ival(d.i))))>,1)
                >,<>)

    State1 = (1,<(andf(ch(press),Ival(press)), progress,
                 <(en.(i+1),andf(Ival(en.i),eqf(Ival(key),Ival(d.i))))>,1)
                 >,<>)

within {State0,State1}

Digit_g(i) = (sg_digit(i),Digit.i,0,{en.i,en.i+1,press})

sg_km = 
  let
    State0 = (0,<(TRUE,progress, <(press,FALSE)>,1)>,<>)

    State1 = (1,<(andf(ch(press),Ival(press)), progress,
                <(press,FALSE)>,1)>,<>)
   
within {State0, State1}

KeyMan = (sg_km,Key_Man,0,{press})