#!./preprocessor.py
% CHIRP: 11
% CAS: 30
% Frame: 40 (Header) + 16*N (Payload) + 24 (CRC), 0 <= N < 128
% NIT: Absolute minimum: bit @ 0.4µs, MT at 1µs, NIT at 2MT.
%
%

% Additional rules for if, to reduce the size of the linearised process.
var a, b: Bool;
eqn if(a, false, true) = !a;
    if(a, b, true) = a => b;
    if(a, b, false) = a && b;
    if(a, true, b) = a || b;

% User defined sorts
sort Sender = Nat; 
     Signal = struct NONE?isNone 
                   | NOISE?isNoise 
                   | DATA_BIT(s: Sender)?isData 
                   | CAS_BIT?isCAS 
                   | FIRST_HEADER_BIT(s: Sender)?isHeader 
                   | FIRST_BODY_BIT(s: Sender)?isBody;
     Symbol = struct CHIRP  
                   | IDLE_END 
                   | CAS
                   | FRAME(s: Sender)?isFrame
                   | FRAME_HEADER(s: Sender)?isHeader 
                   | NOTHING;

% Model parameters
map deaf_node,            
    mute_node,            
    reset_node: Sender;   
    SLOT_length,
    MIN_DELAY,            
    MAX_DELAY: Nat;
    CHIRP_length: Nat;    
    ATTEMPTS,
    NIT_length,
    CYCLE_length: Pos;
    AP_offset: Nat;
    length: Symbol -> Nat;
    noise_max_burst,
    noise_min_backoff,
    noise_max_backoff: Nat;
var id: Sender;
eqn ATTEMPTS = ${ATTEMPTS};
    deaf_node = ${DEAF};      % Which is the deaf node (0 to disable)
    mute_node = ${MUTE};      % Which is the mute node (0 to disable)
    reset_node = ${RESET};    % Which is the resetting node (0 to disable)
    MIN_DELAY = ${MIN_DELAY}; % Min and max delay of delayed nodes
    MAX_DELAY = ${MAX_DELAY}; 
    AP_offset = ${AP_OFFSET};
    SLOT_length = ${SLOT_LENGTH};
    CHIRP_length = ${CHIRP};  % Lengths (in bits) of CHIRP, NIT, CAS, 
    NIT_length = ${NIT};      %   frame header and frame
    length(CAS) = ${CAS}; 
    length(FRAME_HEADER(id)) = ${HDR}; 
    length(FRAME(id)) = ${HDR} + ${PAYLOAD}; 
    length(NOTHING) = 0;
    noise_max_burst = ${NOISE_MAX_BURST};     % Noise model
    noise_min_backoff = ${NOISE_MIN_BACKOFF};
    noise_max_backoff = ${NOISE_MAX_BACKOFF};
    
% Model constants and helper functions
map NODES: Pos;
    FRM_START: Sender -> Nat;
    symbol: Signal -> Symbol;
    signal: Symbol -> Signal;
    noise_id: Nat;
var id: Sender;
eqn NODES = 3;   
    noise_id = NODES + 1;
    CYCLE_length = NODES * SLOT_length + NIT_length;
    FRM_START(id) = Int2Nat(id - 1) * SLOT_length + AP_offset;
    symbol(CAS_BIT) = CAS;
    symbol(FIRST_HEADER_BIT(id)) = FRAME_HEADER(id);
    symbol(FIRST_BODY_BIT(id)) = FRAME(id);
    symbol(NOISE) = NOTHING;
    symbol(NONE) = NOTHING;
    signal(CAS) = CAS_BIT;
    signal(FRAME_HEADER(id)) = FIRST_HEADER_BIT(id);
    signal(FRAME(id)) = FIRST_BODY_BIT(id);

act % Bus <--> Node
    get, get', put, put', Get, Put: Sender # Signal;
    % Barrier
    bus: Signal;
    bit, wait;
    Encode: Symbol;
    % MAC <--> CODEC 
    encode: Symbol;
    macCAS, macStart, macStop;
    % CODEC <--> POC
    decode, Decode: Sender # Symbol;
    is_idle, Is_idle: Bool;
    % Events (for debugging and visualisation purposes)
    enter_operation, init_sched, integrating, is_integrating, attempt_startup: Sender;
    abort: Nat;
    reset, Reset: Sender;

% The noise model is parameterised with three values: the maximum length of a 
% noise burst, during which the noise process generates noise. The minimum 
% backoff and maximum backoff bound the period in between bursts.
proc
  Noise = NoiseP(0, 0);
  NoiseP(burst, backoff: Nat) =
      ((backoff >= noise_min_backoff || burst > 0) && burst < noise_max_burst) 
      -> put(noise_id, NOISE) . 
         NoiseP(burst=burst + 1, backoff=0)
  + (backoff <= noise_max_backoff) 
      -> put(noise_id, NONE) . 
         NoiseP(burst=0, backoff=backoff + 1)
  + (burst == noise_max_burst) 
      -> put(noise_id, NONE) . 
         NoiseP(burst=0, backoff=1)
  + sum s: Signal . get(noise_id, s) . NoiseP();

% The bus process is modelled as a discrete-time process that reads from NODES 
% processes and writes the combined signal (two senders results in noise) back 
% to those processes.
map combine: Signal # Signal -> Signal;
var a, b: Signal;
eqn combine(NONE, b) = b;
    combine(a, NONE) = a;
    !(isNone(a) || isNone(b)) -> combine(a, b) = NOISE;
% Two variants are given: one that reads and writes in arbitrary order every bit
% period...
proc
  UnorderedBus(r, w: Set(Sender), nr, nw: Nat, s: Signal) =
  (nr <= NODES) -> (
    sum i: Sender, s': Signal . (!(i in r)) -> put'(i, s') . 
      UnorderedBus(r + {i}, w, nr + 1, nw, 
                   if(i == mute_node, s, combine(s, s')))
  ) <> (
    (nw <= NODES) -> (
      sum i: Sender . (!(i in w)) -> get'(i, if(i == deaf_node, NONE, s)) . 
        UnorderedBus(r, w + {i}, nr, nw + 1, s)
    ) <> (
      bus(s) . UnorderedBus({}, {}, 0, 0, NONE)
    )
  );
% ... and one that does it in a fixed order.
  OrderedBus(r, w: Sender, s: Signal) =
  (r <= NODES + 1) -> (
    sum s': Signal . put'(r, s') . 
      OrderedBus(r + 1, w, if(r == mute_node, s, combine(s, s')))
  ) <> (
    (w <= NODES + 1) -> (
      get'(w, if(w == deaf_node, NONE, s)) . OrderedBus(r, w + 1, s)
    ) <> (
      bus(s) . OrderedBus(1, 1, NONE)
    )
  );
% It should not make a difference which is used, so the UnorderedBus is only 
% there fore debugging purposes.
  Bus = OrderedBus(1, 1, NONE);

% The CODEC process models the SDL process of the same name. We abstract away
% from the process of bitstrobing. What remains is the mutually exclusive 
% sending and receiving of bit patterns.
proc CODEC = nested(id: Sender)
{
  initial state Init() = Receive(0, 0, 0, NONE);
  
  state Receive(lastsender: Sender, idle, data: Nat, sig: Signal) =
    is_idle(idle >= CHIRP_length) . Receive()
  + bit . Receive()
  + put(id, NONE) . Receive()
  + sum S: Symbol . encode(S) . Send(signal(S), 0, length(S))
  + sum S: Signal . get(id, S) . 
    (
      isNone(S) -> Receive(0, if(isNone(sig), 
                           min(CHIRP_length, idle + 1), 1), 0, S)
    + isNoise(S) -> Receive(0, 0, 0, S)
    + isData(S) -> Announce(s(S), 0, if(lastsender == s(S), data+1, 0), sig)
    + isCAS(S) -> Announce(s(S), 0, if(isCAS(sig), data + 1, 1), S)
    + (isHeader(S) || isBody(S)) -> Announce(s(S), 0, 1, S)
    );
  
  state Announce(lastsender: Sender, idle, data: Nat, sig: Signal) =
    is_idle(false) . Announce()
  + (data > 0 && data == length(symbol(sig))) 
      -> decode(id, symbol(sig)) . 
         Receive(sig=if(isHeader(sig), FIRST_BODY_BIT(s(sig)), sig))
      <> Receive();
  
  state Send(sig: Signal, sent, len: Nat) = 
    is_idle(false) . Send()
  + bit . Send()
  + (sent == 0) -> put(id, sig) . Send(sent = 1)
  + (sent > 0 && sent < len) 
      -> put(id, if(isCAS(sig), sig, DATA_BIT(id))) . 
         Send(sent = sent + 1)
  + (sent == len && isHeader(sig)) 
      -> put(id, DATA_BIT(id)) . 
         Send(DATA_BIT(id), sent + 1, length(FRAME(id)))
  + (sent == len && !isHeader(sig)) 
      -> sum S: Signal . get(id, S) . Receive(0, 0, 0, NONE)
      <> sum S: Signal . get(id, S) . Send();
};

% The MAC process models the SDL process of the same name, and decides when the
% CODEC process should send data. When it is active, it periodically sends a 
% (startup) frame. If activation is done by a macCAS action, a CAS symbol is 
% sent before activation. The MAC process is deactivated by a macStop action.
proc MAC(id: Sender, togo: Int, active: Bool) =
  macCAS . encode(CAS) . MAC(active=true, togo=FRM_START(id) + SLOT_length - 1)
+ macStart . MAC(active=true, togo=FRM_START(id))
+ macStop . MAC(active=false)
+ active -> (
    (togo > 0) -> (
      wait . MAC(togo=togo - 1)
    ) <> (
      encode(FRAME_HEADER(id)) . MAC(togo=CYCLE_length - 1)
    )
  ) <> wait . MAC();

% The DelayedController models a normal POC process that starts after MIN_DELAY 
% and before MAX_DELAY clock ticks.
proc DelayedController = nested(id: Sender)
{
  initial state Off = Wait(0);  
  
  state Wait(counter: Nat) =
    decode(id, CAS) . Wait()
  + sum id': Sender . 
      decode(id, FRAME_HEADER(id')) . 
      Wait()
  + sum id': Sender . 
      decode(id, FRAME(id')) . 
      Wait()

  + (counter < MAX_DELAY) -> bit . Wait(counter=counter + 1)
  + (counter >= MIN_DELAY) -> Controller(id, ATTEMPTS);
};

% The Controller process models the startup behaviour of the POC SDL process.  
% Its states correspond directly to the SDL states defined in the FlexRay 
% specification.
proc Controller = nested(id: Sender, attempts: Nat)
{
  % StartupPrepare is called every time a startup attempt is initiated. If the
  % number of startup attempts exceeds some maximum (in our case, we choose this
  % maximum to be 3), then startup is aborted altogether.
  initial state StartupPrepare =
    (attempts > 1) -> attempt_startup(id) . ColdstartListen(0, 0)
                   <> integrating(id) . IntegrationListen();

  % In the IntegrationListen state, the node waits for a frame to be decoded
  % from the bus (in this case, the clock synchronisation will have started
  % integration).
  state IntegrationListen() =
    decode(id, CAS) . IntegrationListen()
  + sum id': Sender . decode(id, FRAME_HEADER(id')) . IntegrationListen()
  + sum id': Sender . 
      decode(id, FRAME(id')) . 
      bit . 
      init_sched(id) . 
      InitialiseSchedule(0, id')
  + reset(id) . AbortStartup(attempts=ATTEMPTS)

  + is_integrating(id) . IntegrationListen()

  + bit . IntegrationListen();
  
  % In the ColdStartListen state, the node waits for communication on the bus.
  % If no communication is detected, a coldstart is attempted by sending a CAS
  % symbol (by activating the MAC through a macCAS action).
  state ColdstartListen(tStartup, tStartupNoise: Nat) =
  (
    decode(id, CAS) . ColdstartListen(tStartupNoise=0)
  + sum id': Sender . 
      decode(id, FRAME_HEADER(id')) . 
      ColdstartListen(tStartupNoise=0)
  + sum id': Sender . 
      decode(id, FRAME(id')) . 
      bit . 
      init_sched(id) . 
      InitialiseSchedule(0, id')
  + reset(id) . AbortStartup(attempts=ATTEMPTS)

  + bit . 
    (
      (tStartup >= 2 * CYCLE_length - 1 || 
       tStartupNoise >= 4 * CYCLE_length - 1)
      -> ( is_idle(true) . 
           macCAS . 
           ColdstartCollisionResolution(attempts=Int2Nat(attempts-1), timer=-SLOT_length)
         + is_idle(false) . 
           ColdstartListen(tStartup=0, 
                           tStartupNoise=tStartupNoise + 1)
         )
    + (tStartup < 2 * CYCLE_length - 1 && 
       tStartupNoise < 4 * CYCLE_length - 1)
      -> ( is_idle(true) . 
           ColdstartListen(tStartup=tStartup + 1, 
                           tStartupNoise=tStartupNoise + 1)
         + is_idle(false) . 
           ColdstartListen(tStartup=0, 
                           tStartupNoise=tStartupNoise + 1)
         )
    )
  );

  % In InitialiseSchedule, the node waits for the clock synchronisation process
  % to finish its initialisation. In this model, we abstracted away from clock
  % synchronisation, and therefore this state can be left as soon as the second
  % frame of the sender that this node is synchronising on (syncon) is received.
  state InitialiseSchedule(timer: Nat, syncon: Sender) =
  (
    decode(id, CAS) . InitialiseSchedule()
  + sum id': Sender . 
      decode(id, FRAME_HEADER(id')) . 
      InitialiseSchedule()
  + sum id': Sender . 
      decode(id, FRAME(id')) .
      (
        (id' == syncon) 
        -> ((timer == CYCLE_length - 1) 
            -> bit . 
               IntegrationColdstartCheck(
                 Int2Nat(FRM_START(syncon) + length(FRAME(id'))), syncon, 
                 false, false, false, false)
            <> AbortStartup()
           ) 
        <> InitialiseSchedule()
      )
  + reset(id) . AbortStartup(attempts=ATTEMPTS)
  
  + bit . 
    (timer > CYCLE_length) 
    -> AbortStartup() 
    <> InitialiseSchedule(timer=timer + 1)
  );
  
  % Once a CAS symbol was sent, the ColdStartCollisionResolution state is 
  % entered to see if any other node is taking on the role of leading coldstart
  % node. If not, then this node is the leading coldstart node, and the 
  % ColdstartConsistencyCheck state is entered. Otherwise, startup is aborted.
  state ColdstartCollisionResolution(timer: Int) =
  (
    decode(id, CAS) . AbortStartup()
  + sum id': Sender . 
      decode(id, FRAME_HEADER(id')) . 
      AbortStartup()
  + sum id': Sender . 
      decode(id, FRAME(id')) . 
      ColdstartCollisionResolution()
  + reset(id) . AbortStartup(attempts=ATTEMPTS)
  
  + bit . 
    (timer < CYCLE_length * 4) 
    -> ColdstartCollisionResolution(timer=timer + 1)
    <> ColdstartConsistencyCheck(0, false, false)
  );
  
  % During the ColdstartConsistencyCheck, the node checks that during two
  % consecutive cycles a frame is decoded. If no-one followed, then it is 
  % assumed that the other nodes were not actve yet, and the ColdStartGap state
  % is entered. If in the first cycle a frame is decoded, but not in the second,
  % then it is assumed that something went wrong, and the startup attempt is 
  % simply aborted. If all went well, normal operation is entered.
  state ColdstartConsistencyCheck(timer: Nat, ok1, ok2: Bool) =
  (
    decode(id, CAS) .  ColdstartConsistencyCheck()
  + sum id': Sender . 
      decode(id, FRAME_HEADER(id')) . 
      ColdstartConsistencyCheck()
  + sum id': Sender . 
      decode(id, FRAME(id')) . 
      ColdstartConsistencyCheck(ok1=true, ok2=timer >= CYCLE_length)
  + reset(id) . AbortStartup(attempts=ATTEMPTS)
  
  + (timer < CYCLE_length * 1 - 1) 
    -> bit . ColdstartConsistencyCheck(timer=timer + 1)
  + (timer < CYCLE_length * 2 - 1 && timer >= CYCLE_length * 1 - 1)
    -> (ok1 -> bit . ColdstartConsistencyCheck(timer=timer + 1)
            <> ((attempts > 0) -> macStop . 
                                  ColdstartGap(attempts=Int2Nat(attempts - 1), timer=0)
                               <> bit . AbortStartup()))
  + (timer >= CYCLE_length * 2 - 1)
    -> (ok2 -> bit . enter_operation(id) . NormalOperation()
            <> AbortStartup())
  );
  
  % During the ColdStartGap, no frames are sent for one cycle. After this cycle,
  % frame sending is recommenced, so that other nodes may follow. Entering the
  % ColdStartGap state counts as a new coldstart attempt, and can therefore only
  % be done a limited number of times.
  state ColdstartGap(timer: Nat) =
  (
    decode(id, CAS) .  AbortStartup()
  + sum id': Sender . 
      decode(id, FRAME_HEADER(id')) . 
      AbortStartup()
  + sum id': Sender . 
      decode(id, FRAME(id')) . 
      ColdstartGap()
  + reset(id) . AbortStartup(attempts=ATTEMPTS)
  
  + (timer < CYCLE_length * 1)
    -> bit . ColdstartGap(timer + 1)
    <> macStart . 
       ColdstartCollisionResolution(0)
  );
  
  % The IntegrationColdstartCheck is performed when a node is not the leading
  % coldstart node. It checks that either the leading coldstart node is still
  % sending frames as expected, or otherwise at least two other nodes are 
  % sending frames. If this is not the case, then the coldstart attempt is 
  % aborted.
  state IntegrationColdstartCheck(timer: Nat, syncon: Sender, 
                                  seen1, seen2, ok1, ok2: Bool) =
  (
    decode(id, CAS) .  IntegrationColdstartCheck()
  + reset(id) . AbortStartup(attempts=ATTEMPTS)
  + sum id': Sender . 
      decode(id, FRAME_HEADER(id')) . 
      IntegrationColdstartCheck()
  + sum id': Sender . 
      decode(id, FRAME(id')) . 
      IntegrationColdstartCheck(
        seen1=timer >= 1 * CYCLE_length, 
        ok1=seen1 || (id'==syncon && timer >= 1 * CYCLE_length),
        seen2=timer >= 2 * CYCLE_length, 
        ok2=seen2 || (id'==syncon && timer >= 2 * CYCLE_length))

  + (timer < 1 * CYCLE_length - 1)
    -> bit . IntegrationColdstartCheck(timer=timer + 1)
  + (timer < 2 * CYCLE_length - 1 && timer >= 1 * CYCLE_length - 1) 
    -> bit . IntegrationColdstartCheck(timer=timer + 1)
  + (timer < 3 * CYCLE_length - 1 && timer >= 2 * CYCLE_length - 1) 
    -> (ok1 -> bit . IntegrationColdstartCheck(timer=timer + 1)
            <> bit . AbortStartup())
  + (timer >= 3 * CYCLE_length - 1)
    -> (ok2 -> macStart . 
               attempt_startup(id) . ColdstartJoin(0)
             <> AbortStartup())
  );
  
  % During the ColdstartJoin phase, a coldstart node that is not the leading
  % coldstart node starts sending frames. 
  state ColdstartJoin(timer: Nat) =
  (
    decode(id, CAS) .  ColdstartJoin()
  + sum id': Sender . 
      decode(id, FRAME_HEADER(id')) . 
      ColdstartJoin()
  + sum id': Sender . 
      decode(id, FRAME(id')) .  
      ColdstartJoin()
  + reset(id) . AbortStartup(attempts=ATTEMPTS)
  
  + bit . (timer < 3 * CYCLE_length)
    -> ColdstartJoin(timer + 1)
    <> enter_operation(id) . NormalOperation()
  );
  
  % When a startup attempt is aborted, the MAC is stopped and the StartupPrepare
  % state is entered again.
  state AbortStartup() =
  (
    decode(id, CAS) . AbortStartup()
  + sum id': Sender . 
      decode(id, FRAME_HEADER(id')) . 
      AbortStartup()
  + sum id': Sender . 
      decode(id, FRAME(id')) . 
      AbortStartup()
  + reset(id) . AbortStartup(attempts=ATTEMPTS)
  
  + macStop . abort(id) . Controller()
  );
  
  % During normal operation, there is no more controlling behaviour of the POC.
  % We must however actively ignore bit and decode actions to avoid deadlock.
  state NormalOperation() =
    bit . NormalOperation()
  + sum s: Symbol . decode(id, s) . NormalOperation()
  + reset(id) . AbortStartup(attempts=ATTEMPTS);

};


% An absent node is modelled explicitly to be able to reuse this specification
% for two-node scenarios without having to change the number of parallel 
% components.
proc AbsentNode(id: Sender) =
  wait|bit|bit . AbsentNode()
+ sum s: Signal . get(id, s) . AbsentNode()
+ put(id, NONE) . AbsentNode();

% A normal node consists of a CODEC, a MAC and a POC that starts immediately.
proc NormalNode(id: Sender) =
  allow({wait|bit|bit, Encode|bit, get, put, Decode, Is_idle, macCAS|macCAS, 
         macStart|macStart, macStop|macStop, enter_operation, integrating, 
         is_integrating, abort, init_sched, reset, attempt_startup},
    comm({encode|encode->Encode, decode|decode->Decode, 
          is_idle|is_idle->Is_idle},
      CODEC(id) || Controller(id, ATTEMPTS) || MAC(id, 0, false)
  ));

% A delayed node consists of a CODEC, a MAC and a POC that starts operation 
% after a bounded initial delay.
proc DelayedNode(id: Sender) =
  allow({wait|bit|bit, Encode|bit, get, put, Decode, Is_idle, macCAS|macCAS, 
         macStart|macStart, macStop|macStop, enter_operation, integrating, 
         is_integrating, abort, init_sched, reset, attempt_startup},
    comm({encode|encode->Encode, decode|decode->Decode, 
          is_idle|is_idle->Is_idle},
      CODEC(id) || DelayedController(id) || MAC(id, 0, false)
  ));

% If a resetting node is present, then this process controls when it may be 
% reset. For larger statespaces, this process can be changed to restrict the
% frequency with which a node can be reset.
proc Resetter =
  reset(reset_node) . Resetter()
+ bit . Resetter();    

% The system consists of three nodes. Each node is of type Absent, Normal or
% Delayed. The bus|... multi-actions form the clock tick barrier, all other
% actions are either a result of communication between subcomponents, or actions
% that signal relevant events such as failure to start up.
init 
  allow({Get, Put, 
         bus|Encode|Encode|Encode|bit|bit|bit , 
         bus|Encode|Encode|wait|bit|bit|bit |bit, 
         bus|Encode|wait|wait|bit|bit|bit |bit|bit, 
         bus|wait|wait|wait|bit|bit|bit |bit|bit|bit, 
         Decode, Is_idle, init_sched, 
         macCAS|macCAS, macStart|macStart, macStop|macStop, 
         enter_operation, is_integrating|is_integrating, integrating, abort, Reset, attempt_startup},
    comm({get|get'->Get, put|put'->Put, reset|reset->Reset},
      Bus || Noise || Resetter || 
      ${TYPE1}Node(1) || ${TYPE2}Node(2) || ${TYPE3}Node(3)
  ));

% Mappings for the mu-calculus formulae. 
map nextin: Nat # List(Nat) -> Sender;
    inornext: Nat # List(Nat) -> Sender;
    finite: Symbol -> Bool;
    nextsym: Symbol # List(Nat) -> Symbol;
    correct_nodes: Sender -> List(Sender);
    CORRECT_NODES: List(Sender);
    remove: List(Sender) # Sender -> List(Sender);
var s, s2: Sender;
    l: List(Sender);
    sym: Symbol;
eqn nextin(s, l) = inornext((s + 1) mod (NODES + 1), l);
    l != [] && s in l -> inornext(s, l) = s;
    l != [] && !(s in l) -> inornext(s, l) = nextin(s, l);
    finite(sym) = (isHeader(sym) || isFrame(sym)) => s(sym) <= NODES;
    nextsym(FRAME_HEADER(s), l) = FRAME(s);
    nextsym(FRAME(s), l) = FRAME_HEADER(nextin(s, l));
    s <= NODES -> correct_nodes(s) = 
      if(!(s in {reset_node, deaf_node, mute_node}), 
         s |> correct_nodes(s + 1), 
         correct_nodes(s + 1));
    s > NODES -> correct_nodes(s) = [];
    CORRECT_NODES = correct_nodes(0);
    remove(s2 |> l, s) = if(s2 == s, l, s2 |> remove(l, s));
    remove([], s) = [];

