/* Copyright (c) 2000-2019 Ericsson Telecom AB
* All rights reserved. This program and the accompanying materials
* are made available under the terms of the Eclipse Public License v2.0
* which accompanies this distribution, and is available at
* https://www.eclipse.org/org/documents/epl-2.0/EPL-2.0.html
*
* Contributors:
* Michael Josenhans
******************************************************************************/
//
//  File:               J1939test.ttcn
//  Description:        J1939 port type test
//


module Isobus_test {

import from SocketCAN_Types all;
import from SocketCAN_PortType all;
import from SocketCAN_Templates all;
import from J1939 all;
import from IsobusVT_Templates all;
import from Isobus all;

template WorkingSetMaintenanceMessages t_WorkingSetMaintenanceTick(template boolean p_tickvalue) := 
{workingSetMaintenanceTick := p_tickvalue}

template WorkingSetMaintenanceMessages t_WorkingSetMaintenanceInitialize(template boolean p_tickvalue) := 
{workingSetMaintenanceInitialize := p_tickvalue}
const float c_guard := 50.0

type enumerated SocketCAN_open_socket_type
{ 
  OPEN_CAN_RAW,
  OPEN_CAN_BCM,
  OPEN_CAN_ISOTP,
  OPEN_CAN_J1939
}

type enumerated e_Phase {
  e_open_socket, 
  e_testbody1, 
  e_testbody2,
  e_testbody3,
  e_testbody4,
  e_testbody5,
  e_testbody6,
  e_testbody7,
  e_testbodyEnd,
  e_testcase_complete
}

type record SocketCAN_open_j1939_result{
  SocketCAN_ifr                    ifr,
  SocketCAN_socketid               socket_id} 

type record J1939_message  {
  e_Phase phase,
  SocketCAN_J1939_PDU j1939_pdu
}

const integer J1939_MAX_PDU_NUMBER := 256;  // for testing purposes

type record length (0 .. J1939_MAX_PDU_NUMBER) of SocketCAN_J1939_PDU SocketCAN_J1939_PDUs

// workarounds as (x .. enum2int(e_testcase_complete)) fails but:
// workarounds as (x .. enum2int(c_testcase_complete)) works
const e_Phase c_firstPhase        := e_open_socket
const e_Phase c_testcase_complete := e_testcase_complete

type record PhaseStartReq {
  e_Phase phase,
  integer phase_int
}
type record PhaseEndInd   {
  e_Phase phase, 
  integer phase_int
}

type boolean HaltReq
type boolean HaltInd

type union  Command_MTC2PTC{
  PhaseStartReq                       phaseStartReq,
  HaltReq                             haltReq
}

type union  Command_PTC2MTC{
  PhaseEndInd                         phaseEndInd,
  HaltInd                             haltInd
}

type port SyncMasterPort message {
  out Command_MTC2PTC
  in  Command_PTC2MTC
} with { extension "internal" }

type port SyncSlavePort message {
  in  Command_MTC2PTC
  out Command_PTC2MTC
} with { extension "internal" }

type port J1939PDU_PT message {
  inout   J1939PDU_with_NAME
} with { extension "internal" }

type boolean PoolUploadOngoing

type port PoolUploadOngoingIn message {
  in   PoolUploadOngoing
} with { extension "internal" }

type port PoolUploadOngoingOut message {
  out   PoolUploadOngoing
} with { extension "internal" }

type boolean VTStatusTick

type port VTStatusTickIn message {
  in   VTStatusTick
} with { extension "internal" }

type port VTStatusTickOut message {
  out   VTStatusTick
} with { extension "internal" }

type boolean WorkingSetMaintenaceOnOff

type port WorkingSetMaintenaceOnOffIn message {
  in   WorkingSetMaintenaceOnOff
} with { extension "internal" }

type port WorkingSetMaintenaceOnOffOut message {
  out   WorkingSetMaintenaceOnOff
} with { extension "internal" }

type union WorkingSetMaintenanceMessages
{
  // put all workingSetMaintenance messages here
  boolean               workingSetMaintenanceTick,
  boolean               workingSetMaintenanceInitialize
}

type port WorkingSetMaintenanceIn message {
  in   WorkingSetMaintenanceMessages
} with { extension "internal" }

type port WorkingSetMaintenanceOut message {
  out   WorkingSetMaintenanceMessages
} with { extension "internal" }

//component declarations

type component SyncPTC {
  port SyncSlavePort                      pt_sync
  var  e_Phase                            v_phase := c_firstPhase
}

type component PTC_Isobus_VT_VTSTATUSCycleSend_CT extends SyncPTC
{
  port VTStatusTickOut                    pt_VTStatusTick
  port PoolUploadOngoingIn                pt_PoolUploadOngoing
  //variables
  //timers
}

type component PTC_Isobus_ECU_VTSTATUSCycleReceive_CT extends SyncPTC
{
  port VTStatusTickIn                     pt_VTStatusTick
  port WorkingSetMaintenaceOnOffOut       pt_WorkingSetMaintenaceOnOff
  //variables
  //timers
}

type component PTC_Isobus_ECU_WorkingSetMaintenanceIndCycleSend_CT extends SyncPTC
{
  port WorkingSetMaintenaceOnOffIn        pt_WorkingSetMaintenaceOnOff
  port WorkingSetMaintenanceOut           pt_WorkingSetMaintenance
  //timers
}

type component PTC_Isobus_VT_CT extends SyncPTC
{
  port J1939PDU_PT                        pt_j1939PDU
  port VTStatusTickIn                     pt_VTStatusTick
  //variables
  var J1939_ADDR v_peeraddr := J1939_NO_ADDR
  var J1939_NAME v_peername := J1939_NO_NAME
  //timers
}

type component PTC_Isobus_ECU_CT extends SyncPTC
{
  port J1939PDU_PT                        pt_j1939PDU
  port WorkingSetMaintenanceIn            pt_WorkingSetMaintenance
  port VTStatusTickOut                    pt_VTStatusTick
  //variables
  var J1939_ADDR v_peeraddr := J1939_NO_ADDR
  var J1939_NAME v_peername := J1939_NO_NAME
  //timers
}

type component PTCAdapter extends SyncPTC {
  port SocketCAN_PT                       pt_socketCAN
  port J1939PDU_PT                        pt_j1939PDU
}

type record of PTCs PTCSet 

type union  PTCs{
  PTCAdapter                                          ptc_Adapter,
  PTC_Isobus_VT_VTSTATUSCycleSend_CT                  ptc_Isobus_VT_VTSTATUSCycleSend_CT,
  PTC_Isobus_VT_CT                                    ptc_Isobus_VT_CT,
  PTC_Isobus_ECU_CT                                   ptc_Isobus_ECU_CT, 
  PTC_Isobus_ECU_VTSTATUSCycleReceive_CT              ptc_Isobus_ECU_VTSTATUSCycleReceive_CT,
  PTC_Isobus_ECU_WorkingSetMaintenanceIndCycleSend_CT ptc_Isobus_ECU_WorkingSetMaintenanceIndCycleSend_CT
}


type component MTC{ 
  timer t_guard
  port  SyncMasterPort pt_sync
  var PTCSet         v_PTCSet := {}
}

altstep alt_awaitPhaseStartReq(in e_Phase p_phase) runs on SyncPTC {
  var Command_MTC2PTC v_PhaseStartReq;
  [] pt_sync.receive (Command_MTC2PTC:{phaseStartReq:={phase := p_phase, phase_int := ?}}){
    log("PTC name: ", self)
    log("Waits for start of phase: ", p_phase)
  }
  // between v_phase and p_phase
  [] pt_sync.receive (Command_MTC2PTC:{phaseStartReq:={phase := ?, phase_int := (enum2int(c_firstPhase) .. enum2int(v_phase))}}) -> value v_PhaseStartReq 
  { 
    //v_phase := f_incPhase(v_phase)
    log("PTC name: ", self)
    log("Waits for start of phase: ", p_phase)
    log("Received completion of phase: ", p_phase)
    f_sendPhaseEndInd()
    repeat
  }
  [] pt_sync.receive (Command_MTC2PTC:{phaseStartReq:={phase := ?, phase_int :=?}}) -> value v_PhaseStartReq
  {log("Received unexpected message:", v_PhaseStartReq);setverdict(inconc)}
}

function f_startPhase (in e_Phase p_phase) runs on MTC {
  var integer v_i
  var integer v_amount := sizeof(v_PTCSet)
  var Command_MTC2PTC v_phaseStartReq := {phaseStartReq:={ phase := p_phase, phase_int := enum2int(p_phase)}}

  for (v_i := 0; v_i < v_amount; v_i := v_i +1){
    log("MTC instance: ", self)
    if        (ischosen(v_PTCSet[v_i].ptc_Adapter))   { pt_sync.send(v_phaseStartReq) to v_PTCSet[v_i].ptc_Adapter}
    else if   (ischosen(v_PTCSet[v_i].ptc_Isobus_VT_VTSTATUSCycleSend_CT)) { pt_sync.send(v_phaseStartReq) to v_PTCSet[v_i].ptc_Isobus_VT_VTSTATUSCycleSend_CT}
    else if   (ischosen(v_PTCSet[v_i].ptc_Isobus_VT_CT)) { pt_sync.send(v_phaseStartReq) to v_PTCSet[v_i].ptc_Isobus_VT_CT}
    else if   (ischosen(v_PTCSet[v_i].ptc_Isobus_ECU_CT)){ pt_sync.send(v_phaseStartReq) to v_PTCSet[v_i].ptc_Isobus_ECU_CT}
    else if   (ischosen(v_PTCSet[v_i].ptc_Isobus_ECU_VTSTATUSCycleReceive_CT)) { pt_sync.send(v_phaseStartReq) to v_PTCSet[v_i].ptc_Isobus_ECU_VTSTATUSCycleReceive_CT}
    else if   (ischosen(v_PTCSet[v_i].ptc_Isobus_ECU_WorkingSetMaintenanceIndCycleSend_CT)){ pt_sync.send(v_phaseStartReq) to v_PTCSet[v_i].ptc_Isobus_ECU_WorkingSetMaintenanceIndCycleSend_CT}
    else {
      log("Chosen PTC type misssing, please add handling for all PTC types!");
      setverdict(inconc)}//something wrong, this should not happen
  }
}

function f_haltAllComponents () runs on MTC {
  var integer v_i
  var integer v_amount := sizeof(v_PTCSet)
  var Command_MTC2PTC v_haltReq := {haltReq:=true}
  for (v_i := 0; v_i < v_amount; v_i := v_i +1){
    log("MTC instance: ", self)
    if        (ischosen(v_PTCSet[v_i].ptc_Adapter))   { pt_sync.send(v_haltReq) to v_PTCSet[v_i].ptc_Adapter}
    else if   (ischosen(v_PTCSet[v_i].ptc_Isobus_VT_VTSTATUSCycleSend_CT)) { pt_sync.send(v_haltReq) to v_PTCSet[v_i].ptc_Isobus_VT_VTSTATUSCycleSend_CT}
    else if   (ischosen(v_PTCSet[v_i].ptc_Isobus_VT_CT)) { pt_sync.send(v_haltReq) to v_PTCSet[v_i].ptc_Isobus_VT_CT}
    else if   (ischosen(v_PTCSet[v_i].ptc_Isobus_ECU_CT)){ pt_sync.send(v_haltReq) to v_PTCSet[v_i].ptc_Isobus_ECU_CT}
    else if   (ischosen(v_PTCSet[v_i].ptc_Isobus_ECU_VTSTATUSCycleReceive_CT)) { pt_sync.send(v_haltReq) to v_PTCSet[v_i].ptc_Isobus_ECU_VTSTATUSCycleReceive_CT}
    else if   (ischosen(v_PTCSet[v_i].ptc_Isobus_ECU_WorkingSetMaintenanceIndCycleSend_CT)){ pt_sync.send(v_haltReq) to v_PTCSet[v_i].ptc_Isobus_ECU_WorkingSetMaintenanceIndCycleSend_CT}
    else {
      log("Chosen PTC type misssing, please add handling for all PTC types!");
      setverdict(inconc)}//something wrong, this should not happen
  }
}

function f_incPTCPhase(in e_Phase p_currentPhase) runs on SyncPTC return e_Phase {
  var e_Phase v_nextPhase
  log("PTC: ", self)
  log("PTC instance: ", self)
  log("Current PTC phase: ", p_currentPhase)
  int2enum( enum2int(p_currentPhase)+1, v_nextPhase)
  log("Next PTC phase:", v_nextPhase)
  return v_nextPhase
}

function f_sendPhaseEndInd() runs on SyncPTC{
  // just to allow matching with integer ranges on the reception side, as it is not poosible to do so with enums
  var Command_PTC2MTC v_PhaseEndInd := {phaseEndInd :={phase := v_phase, phase_int := enum2int(v_phase)}}
  pt_sync.send(v_PhaseEndInd)
  log("PTC: PhaseEndInd to MTC with content: ", v_PhaseEndInd, self)
  v_phase := f_incPTCPhase(v_phase)
}

function f_addSyncSlaveSet (in PTCs p_slave,
  inout PTCSet p_set) {
  p_set[sizeof(p_set)] := p_slave
  return
}
function f_incMTCPhase(in e_Phase p_currentPhase) runs on MTC return e_Phase {
  var e_Phase v_nextPhase
  log("MTC: ", self)
  log("Current phase: ", p_currentPhase)
  int2enum( enum2int(p_currentPhase)+1, v_nextPhase)
  log("Next phase:", v_nextPhase)
  return v_nextPhase
}

function f_awaitEndPhase(in e_Phase p_phase) runs on MTC {
  var integer v_amount:= sizeof(v_PTCSet);
  var integer v_i
  t_guard.start(c_guard)
  var Command_PTC2MTC v_PhaseEndInd

  log("Available PTCs", v_PTCSet)

  for(v_i := 0; v_i < v_amount; v_i := v_i +1) {
    alt {
      [] pt_sync.receive (Command_PTC2MTC:{phaseEndInd:= {phase :=p_phase, phase_int := ?}}) -> value v_PhaseEndInd
      {
        log("Nth PTC", v_i, "of n PTCs: ", v_amount, "Ended phase: ", v_PhaseEndInd.phaseEndInd.phase)
      }
      // value between p_phase +1  and e_testcase_complete:
      [] pt_sync.receive (Command_PTC2MTC:{phaseEndInd:= {phase :=?, phase_int :=  (enum2int(p_phase) .. (enum2int(c_testcase_complete)))}}) -> value v_PhaseEndInd
      {
        log("Nth PTC", v_i, "of n PTCs: ", v_amount, "Ended phase: ", v_PhaseEndInd.phaseEndInd.phase)
      }
      [] t_guard.timeout {
        log("Timeout in MTC phase:", p_phase)
        setverdict(inconc)
      }
      [] pt_sync.receive (Command_PTC2MTC:{phaseEndInd:=?})  -> value v_PhaseEndInd {
        log("Unexpected phase recieved: ", v_PhaseEndInd)
        log("Expected phase range: ", p_phase)
        log(" to ", c_testcase_complete)
        setverdict(inconc)        
      }
      [] any port.receive{
        log("Expected phase:", p_phase)
        setverdict(inconc)
      }

    } 
  }
  t_guard.stop
}

function f_awaitAllComponentsHalt() runs on MTC {
  var integer v_amount:= sizeof(v_PTCSet);
  var integer v_i
  t_guard.start(c_guard)

  for(v_i := 0; v_i < v_amount; v_i := v_i +1) {
    alt {
      [] pt_sync.receive (Command_PTC2MTC:{haltInd :=?}){
      }
      [] t_guard.timeout {
        log("Timeout in MTC while waiting for command HaltRes")
        setverdict(inconc)
      }
      [] any port.receive{
        log("Received unexpeced message")
        setverdict(inconc)
      }
    } 
  }
  t_guard.stop
}
function f_open_socket(in SocketCAN_socket p_socket) 
runs on PTCAdapter 
return SocketCAN_socket_result {

  var SocketCAN_socket_result v_result  
  timer t_guard
  t_guard.start(c_guard)

  pt_socketCAN.send(p_socket)  

  // receive response
  alt {
    [] pt_socketCAN.receive(
      a_SocketCAN_socket_result(a_result(SocketCAN_SUCCESS))) -> value v_result
    {log("SocketCan:Socket opened: ", v_result.id)}
    [] pt_socketCAN.receive(a_SocketCAN_socket_result(a_result(SocketCAN_ERROR)))
    {log("Received Opening Socket failed"); setverdict(fail)}
    [] t_guard.timeout {
      log("guard timeout!")
      setverdict(fail)}
  }
  t_guard.stop
  return v_result
}

function f_ioctl_get_if_index(in SocketCAN_socketid p_socket_id) 
runs on PTCAdapter 
return SocketCAN_ioctl_result {
  var SocketCAN_ioctl_result v_result   
  timer t_guard
  t_guard.start(c_guard)

  pt_socketCAN.send(SocketCAN_ioctl:{id:= p_socket_id, ifu := omit});
  // receive response
  alt {
    [] pt_socketCAN.receive(a_SocketCAN_ioctl_result(a_result(SocketCAN_SUCCESS))) -> value v_result
    {log("Retrieved interface index", v_result.ifr.if_index)}
    [] pt_socketCAN.receive(a_SocketCAN_ioctl_result(a_result(SocketCAN_ERROR)))
    {log("Retrieving interface index failed", p_socket_id); setverdict(fail)}       
    [] t_guard.timeout {
      log("guard timeout!")
      setverdict(fail)
    }
  } 
  t_guard.stop
  return v_result
}

function f_connect(in SocketCAN_socketid p_socket_id,
  in SocketCAN_if_index p_if_index, 
  in J1939_NAME p_j1939_name_destination,
  in J1939_PGN  p_j1939_pgn_destination,
  in J1939_ADDR  p_j1939_pgn_addr)
runs on PTCAdapter 
return SocketCAN_connect_result {  
  var SocketCAN_connect_result v_result                   
  timer t_guard
  t_guard.start(c_guard)

  pt_socketCAN.send(SocketCAN_Types.SocketCAN_connect:{id:= p_socket_id, 
      connectu := {j1939 := {if_index:= p_if_index, 
          j1939_destination:= {
            name := p_j1939_name_destination /* or J1939_NO_NAME */,
            pgn  := p_j1939_pgn_destination /* or J1939_NO_PGN */, 
            addr := p_j1939_pgn_addr        /* or J1939_NO_ADDR */}}}});
  // SocketCAN_connect receive response
  alt {
    [] pt_socketCAN.receive(a_SocketCAN_connect_result(a_result(SocketCAN_SUCCESS))) -> value v_result
    {log("Connecting socket", p_socket_id)}
    [] pt_socketCAN.receive(a_SocketCAN_connect_result(a_result(SocketCAN_ERROR))) 
    {log("Connecting socket failed.", p_socket_id); setverdict(fail)}       
    [] t_guard.timeout {
      log("guard timeout!")
      setverdict(fail)}
  } 
  t_guard.stop
  return v_result
}

function f_bind(
  in SocketCAN_socketid p_socket_id,
  in SocketCAN_if_index p_if_index, 
  in J1939_NAME         p_j1939_name_source,
  in J1939_PGN          p_j1939_pgn_source,
  in J1939_ADDR         p_j1939_addr_source) 
runs on PTCAdapter 
return SocketCAN_bind_result {
  var SocketCAN_bind_result v_result
  timer t_guard
  t_guard.start(c_guard)

  log("p_socket_id", p_socket_id)
  log("p_if_index", p_if_index)
  log("p_j1939_name_source", p_j1939_name_source)
  log("p_j1939_pgn_source", p_j1939_pgn_source)
  log("p_j1939_addr_source", p_j1939_addr_source)


  pt_socketCAN.send(SocketCAN_bind:{id:= p_socket_id, 
      bindu := {j1939 := {if_index:= p_if_index, 
          j1939_source:= 
          {name :=  p_j1939_name_source /* or J1939_NO_NAME */,
            pgn :=  p_j1939_pgn_source  /* or J1939_NO_PGN */, 
            addr := p_j1939_addr_source /* or J1939_NO_ADDR or J1939_IDLE_ADDR */ }}}});
  alt {
    [] pt_socketCAN.receive(a_SocketCAN_bind_result(a_result(SocketCAN_SUCCESS))) -> value v_result
    {log("Binding socket", p_socket_id)}
    [] pt_socketCAN.receive(a_SocketCAN_bind_result(a_result(SocketCAN_ERROR))) {}
    [] t_guard.timeout {
      log("guard timeout!")
      setverdict(fail)
    }
  }
  t_guard.stop
  return v_result
}

function f_j1939_send_data_to(
  in SocketCAN_socketid   p_socket_id, 
  in SocketCAN_if_index   p_if_index,
  in J1939_hdr            p_j1939_destination,
  in SocketCAN_J1939_PDU  p_pdu)
runs on PTCAdapter
return SocketCAN_j1939_send_data_to_result { 
  var SocketCAN_j1939_send_data_to_result v_result

  timer t_guard
  t_guard.start(c_guard)

  pt_socketCAN.send(SocketCAN_j1939_send_data_to:{
      id                := p_socket_id,
      if_index          := p_if_index,
      j1939_destination := p_j1939_destination,
      pdu               := p_pdu});

  alt {
    [] pt_socketCAN.receive(a_SocketCAN_j1939_send_data_to_result(a_result(SocketCAN_SUCCESS))) -> value v_result
    {log("Sending j1939_send_data_to", p_socket_id)}
    [] pt_socketCAN.receive(a_SocketCAN_j1939_send_data_to_result(a_result(SocketCAN_ERROR))) 
    {log("Sending j1939_send_data_to failed", p_socket_id); setverdict(fail)}       
    [] t_guard.timeout {
      log("guard timeout!")
      setverdict(fail)
    }
  }
  t_guard.stop
  return v_result
}

function f_j1939_send_data(in SocketCAN_socketid p_socket_id, 
  in SocketCAN_J1939_PDU              p_pdu) 
runs on PTCAdapter 
return SocketCAN_j1939_send_data_result { 

  var SocketCAN_j1939_send_data_result v_result

  timer t_guard
  t_guard.start(c_guard)
  log("SocketCAN_j1939_send_data_to:{id}:", p_socket_id)
  log("SocketCAN_j1939_send_data_to:{pdu}:", p_pdu)

  pt_socketCAN.send(SocketCAN_j1939_send_data:{
      id:= p_socket_id, 
      pdu:=p_pdu});
  alt {
    [] pt_socketCAN.receive(a_SocketCAN_j1939_send_data_result(a_result(SocketCAN_SUCCESS))) -> value v_result
    {log("Writing data on J1939 socket: ", p_socket_id)}
    [] pt_socketCAN.receive(a_SocketCAN_j1939_send_data_result(a_result(SocketCAN_ERROR))) 
    {log("Writing data on J1939 socket failed", p_socket_id); 
      setverdict(fail)}       
    [] t_guard.timeout {
      log("guard timeout!")
      setverdict(fail)}
  }
  t_guard.stop
  return v_result
}

function f_setsockopt(in SocketCAN_socketid p_socket_id,
  in SocketCAN_setsockopt_commandu p_command)
runs on PTCAdapter 
return SocketCAN_setsockopt_result{
  var SocketCAN_setsockopt_result v_result

  timer t_guard
  t_guard.start(c_guard)

  pt_socketCAN.send(SocketCAN_Types.SocketCAN_setsockopt:{id:= p_socket_id, command := p_command});
  alt {
    [] pt_socketCAN.receive(a_SocketCAN_setsockopt_result(a_result(SocketCAN_SUCCESS))) -> value v_result
    {log("Writing data", p_socket_id)}
    [] pt_socketCAN.receive(a_SocketCAN_setsockopt_result(a_result(SocketCAN_ERROR))) 
    {log("Writing data failed", p_socket_id); setverdict(fail)}       
    [] t_guard.timeout {
      log("guard timeout!")
      setverdict(fail)
    }
  }
  t_guard.stop
  return v_result
}

function f_close_socket (in SocketCAN_socketid p_socket_id) 
runs on PTCAdapter {
  pt_socketCAN.send(SocketCAN_close:{id:= p_socket_id});
}

function f_open_j1939()
runs on PTCAdapter 
return SocketCAN_open_j1939_result {
  var SocketCAN_socketid v_socket_id
  v_socket_id := f_open_socket({domain:=PF_CAN, ptype := SOCK_DGRAM, protocol:= CAN_J1939}).id
  var SocketCAN_ifr v_ifr
  v_ifr := f_ioctl_get_if_index(v_socket_id).ifr

  var SocketCAN_open_j1939_result v_result
  v_result := {ifr := v_ifr, socket_id := v_socket_id}

  return v_result
}

function f_ptc_J1939Adapter(
  in e_Phase             p_phase,
  in J1939_Priority      p_send_prio,
  in J1939_NAME          p_j1939_name_source) runs on PTCAdapter {
  map(self:pt_socketCAN, system:pt_socketCAN)
  var SocketCAN_socketid v_socket_id
  var SocketCAN_ifr v_ifr

  alt_awaitPhaseStartReq(e_open_socket)
  var SocketCAN_open_j1939_result res
  res := f_open_j1939()
  v_socket_id := res.socket_id
  v_ifr := res.ifr
  var SocketCAN_bind_result v_bind_result
  v_bind_result := f_bind(v_socket_id,
    v_ifr.if_index, 
    p_j1939_name_source, 
    J1939_NO_PGN,  /* p_j1939_pgn_source */
    J1939_NO_ADDR  /* p_j1939_addr_source */)
  var SocketCAN_setsockopt_result            v_setsockopt_result
  v_setsockopt_result := f_setsockopt(v_socket_id, {j1939_prio:=p_send_prio})
  const SocketCAN_setsockopt_commandu c_commandu_activate_broadcast := {j1939_broadcast := Enable} 
  // configure broadcast:
  v_setsockopt_result := f_setsockopt(v_socket_id, c_commandu_activate_broadcast)
  f_sendPhaseEndInd() //e_open_socket
  alt_awaitPhaseStartReq(p_phase)
  f_sendPhaseEndInd()
  alt_awaitPhaseStartReq(e_testbodyEnd)
  f_sendPhaseEndInd()


  var SocketCAN_receive_j1939_message v_result
  var SocketCAN_j1939_send_data_to_result v_send_data_to_result
  var J1939PDU_with_NAME v_pgn_and_pdu_with_name
  var boolean condition := true
  var boolean v_guard :=true

  timer t_guard


  while (condition)
  {
    alt 
    {
      [] pt_sync.receive (Command_MTC2PTC:{haltReq:=?}){

        pt_sync.send(Command_PTC2MTC:{haltInd:=true})
        log("PTC name: ", self)
        log("Got HaltReq command")
        condition := false
      }

      [v_guard] pt_j1939PDU.receive(J1939PDU_with_NAME:{addr:= ?, name:=?,pdu:=?}) 
      -> value v_pgn_and_pdu_with_name 
      { 
        t_guard.start(c_guard)

        var octetstring v_j1939_pdu, v_pgn_and_pdu
        v_pgn_and_pdu := f_encode_J1939_message (v_pgn_and_pdu_with_name.pdu)
        v_j1939_pdu := substr(v_pgn_and_pdu,3,lengthof(v_pgn_and_pdu)-3)// strip PGN

        var J1939_hdr v_j1939_destination := {
          name := v_pgn_and_pdu_with_name.name, 
          pgn := substr(v_pgn_and_pdu,0,3),        // strip PDU,  pgn_destination 
          addr:= v_pgn_and_pdu_with_name.addr
        }


        pt_socketCAN.send(SocketCAN_j1939_send_data_to:{
            id                := v_socket_id,
            if_index          := v_ifr.if_index,
            j1939_destination := v_j1939_destination,
            // strip PGN
            pdu               := v_j1939_pdu});

        v_guard:=false;  //stop receiving until send confirmation received 
      }

      [not(v_guard)] pt_socketCAN.receive(a_SocketCAN_j1939_send_data_to_result(a_result(SocketCAN_SUCCESS))) -> value v_send_data_to_result
      {
        log("Sending j1939_send_data_to:", v_socket_id, ", ", v_ifr.if_index)
        v_guard:=true
        t_guard.stop
      }

      [not(v_guard)] pt_socketCAN.receive(a_SocketCAN_j1939_send_data_to_result(a_result(SocketCAN_ERROR))) 
      {
        log("Sending j1939_send_data_to failed", v_socket_id); 
        v_guard:=true
        t_guard.stop
        setverdict(fail)
      }

      [] pt_socketCAN.receive(a_SocketCAN_receive_j1939_message(
          v_socket_id,
          v_ifr,
          ?, /* any pgn */
          ?, /* any peer_addr */
          ?, /* any peer_name */
          ?  /* any j1939_pdu */)) -> value v_result
      {
        log("SocketCan:J1939 message from socket received", v_result)     
        pt_j1939PDU.send({addr:=v_result.destAddr, name:= v_result.name, 
            // concatenate received pgn and pdu
            pdu:=f_decode_J1939_message(v_result.pgn & v_result.pdu) /* concatenate pgn & pdu */}); 
      }
      [] pt_sync.receive
      {
        log("Fail:Unexpected message from port pt_sync received");
        setverdict(fail)
      }
      [v_guard] pt_socketCAN.receive
      {
        log("Fail:Unexpected message from port pt_socketCAN received")
        //this should catch any incoming message type not matched on the first alternatives
        setverdict(fail)
      }

      [v_guard] pt_j1939PDU.receive
      {
        log("Fail:Unexpected message from port pt_j1939PDU received")
        //this should catch any incoming message type not matched on the first alternatives
        setverdict(fail)
      }

      [v_guard] any port.receive   
      {
        log("Fail:Message received on a different port")
        //this should catch any incoming message type not matched on the first alternatives on any other port
        setverdict(fail)
      } 

      [not(v_guard)] t_guard.timeout {
        log("guard timeout!")
        setverdict(fail)
      }
    }//endalt
  } // end while


  f_close_socket (v_socket_id)
  unmap(self:pt_socketCAN, system:pt_socketCAN)
  setverdict(pass)
}

function f_ptc_J1939ECUApplication(in e_Phase p_phase) runs on PTC_Isobus_ECU_CT
{

  var boolean condition := true
  alt_awaitPhaseStartReq(p_phase)
  f_sendPhaseEndInd()
  alt_awaitPhaseStartReq(e_testbodyEnd)


  while (condition)
  {
    var J1939PDU_with_NAME v_pgn_and_pdu_with_name  

    alt 
    {
      [] pt_sync.receive (Command_MTC2PTC:{haltReq:=?}){
        pt_sync.send(Command_PTC2MTC:{haltInd:=true})
        log("PTC name: ", self)
        log("Got HaltReq command")
        condition := false
      }

      []pt_j1939PDU.receive(J1939PDU_with_NAME:{addr:= ?, name:=?,
          pdu:=t_VTStatusInd(?, ?, ?, ?, ?)}) -> value v_pgn_and_pdu_with_name 
      { 
        v_peeraddr := v_pgn_and_pdu_with_name.addr
        v_peername := v_pgn_and_pdu_with_name.name
        // store peer name
        //log incoming message 
        log("SocketCan:Expected message VTStatusReq received!", v_pgn_and_pdu_with_name)
        pt_VTStatusTick.send( true );
      }  
      [] pt_WorkingSetMaintenance.receive(t_WorkingSetMaintenanceTick(?)) {
        pt_j1939PDU.send(t_J1939PDU_with_NAME(
            J1939_NO_ADDR, /* set addr 0xFF, applies as name is set */
            v_peername,    /* set peername */
            t_WorkingSetMaintenanceInd(true, compliantWithVTVersion4)

          ))
      }

      []pt_WorkingSetMaintenance.receive(t_WorkingSetMaintenanceInitialize(true)) {
        // the ECU has received the first VTStatus message
        pt_j1939PDU.send(t_J1939PDU_with_NAME(
            J1939_NO_ADDR, /* set addr 0xFF, applies as name is set */
            v_peername,    /* set peername */
            t_GetHardwareReq
          ))    
      }

      []pt_j1939PDU.receive(J1939PDU_with_NAME:{addr:= ?, name:=v_peername,
          pdu:=t_GetHardwareRes(?, ?, ?, ?, ?)}) -> value v_pgn_and_pdu_with_name 
      { 
        log("SocketCan:Expected message GetHardwareRes received!", v_pgn_and_pdu_with_name)
        pt_j1939PDU.send(t_J1939PDU_with_NAME(
            J1939_NO_ADDR, /* set addr 0xFF, applies as name is set */
            v_peername,    /* set peername */
            t_GetNumberOfSoftKeysReq
          ))    
      }  

      []pt_j1939PDU.receive(J1939PDU_with_NAME:{addr:= ?, name:=v_peername,
          pdu:=t_GetNumberOfSoftKeysRes(?, ?, ?, ?, ?)}) -> value v_pgn_and_pdu_with_name 
      { 
        log("SocketCan:Expected message GetNumberOfSoftKeysRes received!", v_pgn_and_pdu_with_name)
        pt_j1939PDU.send(t_J1939PDU_with_NAME(
            J1939_NO_ADDR, /* set addr 0xFF, applies as name is set */
            v_peername,    /* set peername */
            t_GetTextFontDataReq
          ))    
      } 

      []pt_j1939PDU.receive(J1939PDU_with_NAME:{addr:= ?, name:=v_peername,
          pdu:=t_GetTextFontDataRes(?, ?, ?)}) -> value v_pgn_and_pdu_with_name 
      { 
        log("SocketCan:Expected message GetTextFontDataRes received!", v_pgn_and_pdu_with_name)
        pt_j1939PDU.send(t_J1939PDU_with_NAME(
            J1939_NO_ADDR, /* set addr 0xFF, applies as name is set */
            v_peername,    /* set peername */
            t_GetMemoryReq(100000)
          ))    
      } 

      []pt_j1939PDU.receive(J1939PDU_with_NAME:{addr:= ?, name:=v_peername,
          pdu:=t_GetMemoryRes(?, ?)}) -> value v_pgn_and_pdu_with_name 
      { 
        log("SocketCan:Expected message GetMemoryRes received!", v_pgn_and_pdu_with_name)
        log("SocketCan:Sending broken object pool!")
        pt_j1939PDU.send(t_J1939PDU_with_NAME(
            J1939_NO_ADDR, /* set addr 0xFF, applies as name is set */
            v_peername,    /* set peername */
            t_ObjectPoolTransferInd('0123456789ABCDEF'O)))  
        pt_j1939PDU.send(t_J1939PDU_with_NAME(
            J1939_NO_ADDR, /* set addr 0xFF, applies as name is set */
            v_peername,    /* set peername */
            t_EndOfObjectPoolReq))    
      } 

      []pt_j1939PDU.receive(J1939PDU_with_NAME:{addr:= ?, name:=v_peername,
          pdu:=t_EndOfObjectPoolRes(?, ?, ?,               
            /* objectPoolErrorCodes */   { 
              methodOrAttributeNotSupportedByTheVT   :=?,
              unknownObjectReference                 :=true,
              anyOtherError                          :=?,
              objectPoolWasDeletedFromVolatileMemory :=?,
              reserved4                              :=false,
              reserved5                              :=false,
              reserved6                              :=false,
              reserved7                              :=false
            })}) -> value v_pgn_and_pdu_with_name 
      { 
        log("Expected message EndOfObjectPoolRes received!", v_pgn_and_pdu_with_name)
        f_sendPhaseEndInd()

        setverdict ( pass );
      }

      []pt_j1939PDU.receive(J1939PDU_with_NAME:{addr:= ?, name:=v_peername,
          pdu:=t_EndOfObjectPoolRes(?, ?, ?,               
            /* objectPoolErrorCodes */   { 
              methodOrAttributeNotSupportedByTheVT   :=?,
              unknownObjectReference                 :=?,
              anyOtherError                          :=?,
              objectPoolWasDeletedFromVolatileMemory :=?,
              reserved4                              :=false,
              reserved5                              :=false,
              reserved6                              :=false,
              reserved7                              :=false
            })}) -> value v_pgn_and_pdu_with_name 
      { 
        log("Unxxpected message EndOfObjectPoolRes response parameter received!", v_pgn_and_pdu_with_name)
        f_sendPhaseEndInd()

        setverdict ( fail );
      }

      [] pt_j1939PDU.receive(J1939PDU_with_NAME:{addr:=?, name:=?,pdu:=?}) -> value v_pgn_and_pdu_with_name
      {
        log("Unexpected message received!", v_pgn_and_pdu_with_name)
      }

      [] pt_j1939PDU.receive  
      {log("Unexpected message received")} //this should catch any incoming message type not matched on the first alternatives

      //      [] any port.receive   
      //      {
      //        setverdict(fail)        
      //        log("Message received on a different port") //this should catch any incoming message type not matched on the first alternatives on any other port
      //      }
    }//endalt
  } // end while
}

function f_ptc_J1939VTApplication(in e_Phase p_phase) runs on PTC_Isobus_VT_CT
{
  var  boolean  condition := true
  alt_awaitPhaseStartReq(p_phase)
  f_sendPhaseEndInd()
  alt_awaitPhaseStartReq(e_testbodyEnd)


  while (condition)
  {
    var J1939PDU_with_NAME v_pgn_and_pdu_with_name    
    alt 
    {
      [] pt_sync.receive (Command_MTC2PTC:{haltReq:=?}){
        pt_sync.send(Command_PTC2MTC:{haltInd:=true})
        log("PTC name: ", self)
        log("Got HaltReq command")
        condition := false
      }

      []pt_VTStatusTick.receive(VTStatusTick:?)
      {
        pt_j1939PDU.send(t_J1939PDU_with_NAME(
            J1939_NO_ADDR, /* send broadcast, as name is set to J1939_NO_NAME */
            J1939_NO_NAME, /* set peername */
            t_VTStatusInd(J1939_IDLE_ADDR, 
              'FFFF'O, 
              'FFFF'O, 
              vtIsBusyUpdatingVisibleMask, 
              'FF'O)
          ))
      }
      []pt_j1939PDU.receive(J1939PDU_with_NAME:{
          addr := ?, 
          name:=?,
          pdu:=t_WorkingSetMaintenanceInd(?, ?)}) -> value v_pgn_and_pdu_with_name 
      { 
        //log incoming message 
        log("SocketCan:Expected WorkingSetMaintenanceInd message received!", v_pgn_and_pdu_with_name)
        log("The version number is", v_pgn_and_pdu_with_name.pdu.pdu.ecu2vt.workingSetMaintenanceInd.versionNumber)
        v_peeraddr := v_pgn_and_pdu_with_name.addr
        v_peername := v_pgn_and_pdu_with_name.name
        // store peer name
      }  
      []pt_j1939PDU.receive(J1939PDU_with_NAME:{
          addr := ?, 
          name:=?,
          pdu:=t_GetHardwareReq}) -> value v_pgn_and_pdu_with_name 
      { 
        pt_j1939PDU.send(t_J1939PDU_with_NAME(
            v_pgn_and_pdu_with_name.addr, 
            v_pgn_and_pdu_with_name.name,    /* respond to sender */
            t_GetHardwareRes(
              /* bootTimeInSeconds */ 255,
              /* graphicType */ colors256, 
              /* hardware */ { 
                touchScreenandPointingEvent := true, 
                pointingDeviceAndPointingEvent := false, 
                multipleFrequencyAudioOutput := true, 
                adjustableVolumeAudioOutput := true, 
                simultaneousActivationsOfPhysicalSoftKeys := false, 
                simultaneousActivationsOfButtons := false, 
                dragOperationViaPointingEvent := true, 
                intermediateCoordinatesDuringDragOperation := true }, 
              /* xPixels */ 480, 
              /* yPixels */480) 
          ))  
      }
      []pt_j1939PDU.receive(J1939PDU_with_NAME:{
          addr := ?, 
          name:=?,
          pdu:=t_GetNumberOfSoftKeysReq}) -> value v_pgn_and_pdu_with_name 
      { 
        pt_j1939PDU.send(t_J1939PDU_with_NAME(
            v_pgn_and_pdu_with_name.addr, 
            v_pgn_and_pdu_with_name.name,    /* respond to sender */
            t_GetNumberOfSoftKeysRes(
              /* navigationSoftKeys */ '00'O, 
              /* x_dots */ '7D'O, 
              /* y_dots */ '48'O, 
              /* numberOfVirtualSoftKeys */ '40'O , 
              /* numberOfPhysicalSoftKeys */ '0C'O
            )))  
      }

      []pt_j1939PDU.receive(J1939PDU_with_NAME:{
          addr := ?, 
          name:=?,
          pdu:=t_GetTextFontDataReq}) -> value v_pgn_and_pdu_with_name 
      { 
        pt_j1939PDU.send(t_J1939PDU_with_NAME(
            v_pgn_and_pdu_with_name.addr, 
            v_pgn_and_pdu_with_name.name,    /* respond to sender */
            t_GetTextFontDataRes(
              /* small_font_sizes */ { 
                font_8x8 := true, 
                font_8x12 := true, 
                font_12x16 := true, 
                font_16x16 := true, 
                font_16x24 := true, 
                font_24x32 := true, 
                font_32x32 := true, 
                reserved := false }, 
              /* large_font_sizes */ { 
                font_32x48 := true, 
                font_48x64 := true, 
                font_64x64 := true, 
                font_64x96 := true, 
                font_96x128 := true, 
                font_128x128 := true, 
                font_128x192 := true, 
                reserved := false }, 
              /* type_attribute */ { 
                bold_text := true, 
                crossed_out_text := true, 
                underlined_text := true, 
                italics_text := true, 
                inverted_text := true, 
                flash_inverted := true, 
                flash_background_and_foreground := true, 
                proportional_font_rendering := true }
            )))  
      }

      []pt_j1939PDU.receive(J1939PDU_with_NAME:{
          addr := ?, 
          name:=?,
          pdu:=t_GetMemoryReq(?)}) -> value v_pgn_and_pdu_with_name 
      { 
        pt_j1939PDU.send(t_J1939PDU_with_NAME(
            v_pgn_and_pdu_with_name.addr, 
            v_pgn_and_pdu_with_name.name,    /* respond to sender */
            t_GetMemoryRes(
              /* versionNumber */ compliantWithISVersionISO11783_6_2010_E_Second_Edition_version_4, 
              /* status */ thereCanBeEnoughMemory
            )))  
      }

      []pt_j1939PDU.receive(J1939PDU_with_NAME:{
          addr := ?, 
          name:=?,
          pdu:=t_GetVersionsReq}) -> value v_pgn_and_pdu_with_name 
      { 
        pt_j1939PDU.send(t_J1939PDU_with_NAME(
            v_pgn_and_pdu_with_name.addr, 
            v_pgn_and_pdu_with_name.name,    /* respond to sender */
            t_GetVersionsRes(
              /* numberOfVersionStrings */ 0, 
              /* versionStrings */ {  }
            )))  
      }

      []pt_j1939PDU.receive(J1939PDU_with_NAME:{
          addr := ?, 
          name:=?,
          pdu:=t_ObjectPoolTransferInd(?)}) -> value v_pgn_and_pdu_with_name 
      { 
        log("Received Object Pool", v_pgn_and_pdu_with_name.pdu.pdu.ecu2vt.objectPoolTransferInd.objectPoolRecords) 
        log("From addr:", v_pgn_and_pdu_with_name.addr)
        log("From name:", v_pgn_and_pdu_with_name.name)     
      }

      []pt_j1939PDU.receive(J1939PDU_with_NAME:{
          addr := ?, 
          name:=?,
          pdu:=t_EndOfObjectPoolReq}) -> value v_pgn_and_pdu_with_name 
      { 
        pt_j1939PDU.send(t_J1939PDU_with_NAME(
            v_pgn_and_pdu_with_name.addr, 
            v_pgn_and_pdu_with_name.name,    /* respond to sender */
            t_EndOfObjectPoolRes(
              /* errorCodes */ {
                thereAreErrorsInTheObjectPool  := false,
                vtRanOutOfMemoryDuringTransfer := false,
                reserved2                      := false,
                reserved3                      := false,
                anyOtherError                  := false,
                reserved5                      := false,
                reserved6                      := false,
                reserved7                      := false},
              /* parentObjectIDoFaultyObject */ 1,
              /* objectIDofFaultyObject */      2,
              /* objectPoolErrorCodes */   { 
                methodOrAttributeNotSupportedByTheVT   :=false,
                unknownObjectReference                 :=true,
                anyOtherError                          :=false,
                objectPoolWasDeletedFromVolatileMemory :=false,
                reserved4                              :=false,
                reserved5                              :=false,
                reserved6                              :=false,
                reserved7                              :=false
              }
            ))) 
        f_sendPhaseEndInd()

        setverdict ( pass );
      }

      [] pt_j1939PDU.receive(J1939PDU_with_NAME:{addr := ?, name:=?,pdu:=?}) -> value v_pgn_and_pdu_with_name
      {
        log("SocketCan:Unexpected message received!", v_pgn_and_pdu_with_name)
      }

      [] pt_j1939PDU.receive  
      {log("Unexpected message received")} 
      //this should catch any incoming message type not matched on the first alternatives

      [] any port.receive   
      {
        setverdict(fail)
        log("Message received on a different port")} 
      //this should catch any incoming message type not matched on the first alternatives on any other port

    }//endalt
  } // end while

  setverdict(pass)
}


function  f_ptc_J1939VTStatusCycleSend(in e_Phase p_phase)  runs on PTC_Isobus_VT_VTSTATUSCycleSend_CT
{
  //periodic sending
  timer VTStatusClock := 1.0
  var  boolean  condition := true
  alt_awaitPhaseStartReq(p_phase)
  f_sendPhaseEndInd()
  alt_awaitPhaseStartReq(e_testbodyEnd)
  f_sendPhaseEndInd()

  while (condition)
  {
    pt_VTStatusTick.send(true);

    VTStatusClock.start 
    alt
    {
      [] pt_sync.receive (Command_MTC2PTC:{haltReq:=?}){
        pt_sync.send(Command_PTC2MTC:{haltInd:=true})
        log("PTC name: ", self)
        log("Got HaltReq command")
        condition := false
      }

      []VTStatusClock.timeout;
    }
  }//endwhile

  setverdict(pass)

}//endfunction

function  f_ptc_J1939_VTStatusCycleReceive(in e_Phase p_phase)  runs on PTC_Isobus_ECU_VTSTATUSCycleReceive_CT
{

  timer T_VTStatusReceive := 3.0
  var boolean v_VTStatusReceive_running := false
  var boolean condition := true
  //periodic reception

  alt_awaitPhaseStartReq(p_phase)
  f_sendPhaseEndInd()
  alt_awaitPhaseStartReq(e_testbodyEnd)
  f_sendPhaseEndInd()

  while (condition)
  {
    select (v_VTStatusReceive_running) // state
    {
      case (true) {
        alt {
          [] pt_sync.receive (Command_MTC2PTC:{haltReq:=?}){
            pt_sync.send(Command_PTC2MTC:{haltInd:=true})
            log("PTC name: ", self)
            log("Got HaltReq command")
            condition := false
          }

          []pt_VTStatusTick.receive(?) { 
            //log incoming message
            T_VTStatusReceive.stop;
            T_VTStatusReceive.start;
            pt_WorkingSetMaintenaceOnOff.send( true ); 
          } 

          []T_VTStatusReceive.timeout
          {
            pt_WorkingSetMaintenaceOnOff.send( false );
            v_VTStatusReceive_running := false
          }
        }//endalt
      }
      case (false) {
        alt {
          [] pt_sync.receive (Command_MTC2PTC:{haltReq:=?}){
            pt_sync.send(Command_PTC2MTC:{haltInd:=true})
            log("PTC name: ", self)
            log("Got HaltReq command")
            condition := false
          }

          []pt_VTStatusTick.receive(?) { 
            //log incoming message
            T_VTStatusReceive.start;
            v_VTStatusReceive_running := true
            pt_WorkingSetMaintenaceOnOff.send( true ); 
          } 
        } //endalt
      }
    }

  }
  setverdict(pass)

}//endfunction


function  J1939_ECU_WorkingSetMaintenanceIndCycleSend(in e_Phase p_phase)  runs on PTC_Isobus_ECU_WorkingSetMaintenanceIndCycleSend_CT
{
  timer T_WorkingSetMaintenanceIndCycleSend := 1.0
  var boolean  v_WorkingSetMaintenaceOn := false
  var boolean  condition := true

  //periodic reception

  alt_awaitPhaseStartReq(p_phase)
  f_sendPhaseEndInd()
  alt_awaitPhaseStartReq(e_testbodyEnd)
  f_sendPhaseEndInd()

  while (condition)
  {
    select (v_WorkingSetMaintenaceOn) {
      case (true) {
        alt {
          [] pt_sync.receive (Command_MTC2PTC:{haltReq:=?}){
            pt_sync.send(Command_PTC2MTC:{haltInd:=true})
            log("PTC name: ", self)
            log("Got HaltReq command")
            condition := false
          }

          []pt_WorkingSetMaintenaceOnOff.receive(true) 
          // timer already running 
          { 
            //do not do anything
            //log incoming message
          } 
          []pt_WorkingSetMaintenaceOnOff.receive(false) { 
            T_WorkingSetMaintenanceIndCycleSend.stop;
            //log incoming message
            // do not start timer
            v_WorkingSetMaintenaceOn := false // timer is not running
            // trigger ECU reset
          } 
          []T_WorkingSetMaintenanceIndCycleSend.timeout
          {
            // restart timer
            T_WorkingSetMaintenanceIndCycleSend.start
            pt_WorkingSetMaintenance.send( t_WorkingSetMaintenanceTick(true))
          }
        } //endalt
      }
      case (false) {
        alt {
          [] pt_sync.receive (Command_MTC2PTC:{haltReq:=?}){
            pt_sync.send(Command_PTC2MTC:{haltInd:=true})
            log("PTC name: ", self)
            log("Got HaltReq command")
            condition := false
          }

          []pt_WorkingSetMaintenaceOnOff.receive(true) { 
            // timer not running 
            // start timer
            T_WorkingSetMaintenanceIndCycleSend.start
            //log incoming message
            v_WorkingSetMaintenaceOn := true // timer is running
            pt_WorkingSetMaintenance.send( t_WorkingSetMaintenanceTick(true) )
            pt_WorkingSetMaintenance.send( t_WorkingSetMaintenanceInitialize(true) )
          } 
          []pt_WorkingSetMaintenaceOnOff.receive(false) { 
            //timer is stopped
            //log incoming message
            // do not start timer
            // trigger ECU reset
          }
        }
      } //endalt
    }
  }
  setverdict ( pass );
}//endfunction


}