Message Manager model and test gen material

9 files changed, 1887 insertions, 0 deletions

diff --git a/formal/promela/models/messages/README.md b/formal/promela/models/messages/README.md
new file mode 100644
index 00000000..2eb723b5
--- /dev/null
+++ b/formal/promela/models/messages/README.md
@@ -0,0 +1,10 @@
+# Message Manager model
+
+Developer: Eoin Lynch
+
+This directory contains the code for the generation/running of tests for the [RTEMS Message Manager](https://docs.rtems.org/branches/master/c-user/message/index.html)
+
+It is a subset of the material available at [Eoin Lynch's project repository](https://github.com/lynche12/SPIN-PromelaTestGeneration).
+
+This project is research work done for his dissertation as part of the MAI in Computer Engineering program at Trinity College Dublin
+
diff --git a/formal/promela/models/messages/msg-mgr-model-post.h b/formal/promela/models/messages/msg-mgr-model-post.h
new file mode 100644
index 00000000..9a9606d3
--- /dev/null
+++ b/formal/promela/models/messages/msg-mgr-model-post.h
@@ -0,0 +1,8 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+static void Runner( RtemsModelMessageMgr_Context *ctx )
+{
+  T_log( T_NORMAL, "Runner running" );
+  TestSegment3( ctx );
+  T_log( T_NORMAL, "Runner finished" );
+}
diff --git a/formal/promela/models/messages/msg-mgr-model-pre.h b/formal/promela/models/messages/msg-mgr-model-pre.h
new file mode 100644
index 00000000..f3986267
--- /dev/null
+++ b/formal/promela/models/messages/msg-mgr-model-pre.h
@@ -0,0 +1,51 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * @file
+ *
+ * @ingroup RTEMSTestCaseRtemsModelMessageMgr
+ */
+
+/*
+ * Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+ *                    Trinity College Dublin (http://www.tcd.ie)
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ */
+
+/*
+ * This file was automatically generated.  Do not edit it manually.
+ * Please have a look at
+ *
+ * https://docs.rtems.org/branches/master/eng/req/howto.html
+ *
+ * for information how to maintain and re-generate this file.
+ */
+
+#ifndef HAVE_CONFIG_H
+#include "config.h"
+#endif
+
+#include <rtems/score/threadimpl.h>
+
+
+#include "tr-msg-mgr-model.h"
\ No newline at end of file
diff --git a/formal/promela/models/messages/msg-mgr-model-rfn.yml b/formal/promela/models/messages/msg-mgr-model-rfn.yml
new file mode 100644
index 00000000..f5fc8120
--- /dev/null
+++ b/formal/promela/models/messages/msg-mgr-model-rfn.yml
@@ -0,0 +1,202 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+LANGUAGE: C
+
+SEGNAMEPFX: TestSegment{} # segnumber
+SEGARG: Context* ctx
+SEGDECL: static void {}( {} )  # segnamepf{segnumber}, segarg,
+SEGBEGIN: " {"
+SEGEND: "}"
+
+NAME: |
+  /* Test Name is defined in the Test Case code (tc-model-msg-mgr.c) */
+
+semaphore_DCL: rtems_id {0}[SEMA_MAX];
+
+sendrc_DCL: rtems_status_code
+
+recrc_DCL: rtems_status_code
+
+qrc_DCL: rtems_status_code
+
+queue_buffer_DCL: RTEMS_MESSAGE_QUEUE_BUFFER( MAX_MESSAGE_SIZE ) {0} [MAX_PENDING_MESSAGES];
+
+receive_buffer_DCL: uint8_t {0} [ MAX_MESSAGE_SIZE ];
+
+send_buffer_DCL: uint8_t {0} [ MAX_MESSAGE_SIZE ];
+
+send_counter_DCL: uint8_t
+
+INIT: |
+  initialise_semaphore( ctx, semaphore );
+
+Runner: |
+  checkTaskIs( ctx->runner_id );
+
+Worker1: |
+  checkTaskIs( ctx->worker1_id );
+
+Worker2: |
+  checkTaskIs( ctx->worker2_id );
+
+SIGNAL: |
+  Wakeup( semaphore[{}] );
+
+WAIT: |
+  Wait( semaphore[{}] );
+
+message_queue_construct: |
+  T_log( T_NORMAL, "Calling construct(%d,%d,%d,%d,%d)");
+
+  rtems_message_queue_config config;
+  config.name = {3};
+  config.maximum_pending_messages = MAX_PENDING_MESSAGES;
+  config.maximum_message_size = MAX_MESSAGE_SIZE;
+  config.storage_area = queue_buffer;
+  config.storage_size = sizeof( queue_buffer );
+  config.storage_free = NULL;
+  config.attributes = RTEMS_DEFAULT_ATTRIBUTES;
+  
+  {5} = rtems_message_queue_construct(
+    &config,
+    &ctx->queue_id
+  );
+  T_log(T_NORMAL, "Queue id 0x%x", ctx->queue_id);
+  T_log( T_NORMAL, "Returned 0x%x from construct", {5} );
+
+  
+
+message_queue_send: |
+  T_log( T_NORMAL, "Calling Send(%d,%d)");
+
+  memset( send_buffer, {2}, {3} );
+  
+  {4} = rtems_message_queue_send(
+    idNull(ctx, {1}),
+    {2} ? send_buffer : NULL,
+    {3}
+  );
+
+  T_log( T_NORMAL, "Returned 0x%x from send", {4} );
+
+message_queue_receive: |
+  T_log( T_NORMAL, "Calling Receive(%d,%d)");
+  size_t receive_size;
+  {4} = rtems_message_queue_receive(
+  idNull(ctx, {1}),
+  receive_buffer,
+  &receive_size,
+  mergeopts({2}),
+  getTimeout({3})
+  );
+  T_log( T_NORMAL, "Returned 0x%x from receive", {4} );
+
+sendrc:
+  T_rsc( sendrc, {0} );
+
+recrc:
+  T_rsc( recrc, {0} );
+
+qrc:
+  T_rsc( qrc, {0} );
+
+recout:
+  T_eq_int( recout[{0}], {1} );
+
+Ready: |
+   /* We (Task {0}) must have been recently ready because we are running */
+
+Zombie:
+  /* Code to check that Task {0} has terminated */
+
+EventWait:
+  /* Code to check that Task {0} is waiting on events */
+
+TimeWait:
+  /* Code to check that Task {0} is waiting on a timer */
+
+OtherWait:
+  /* Code to check that Task {0} is waiting (after pre-emption) */
+
+SUSPEND:
+  /* SWITCH[{0}] Suspension of proc{1} in favour of proc{2} */
+
+WAKEUP:
+  /* SWITCH[{0}] Wakeup of proc{1} (sometime) after proc{2} */
+  
+LowerPriority: |
+  SetSelfPriority( PRIO_LOW );
+  rtems_task_priority prio;
+  rtems_status_code sc;
+  sc = rtems_task_set_priority( RTEMS_SELF, RTEMS_CURRENT_PRIORITY, &prio );
+  T_rsc_success( sc );
+  T_eq_u32( prio, PRIO_LOW );
+
+EqualPriority: |
+  SetSelfPriority( PRIO_NORMAL );
+  rtems_task_priority prio;
+  rtems_status_code sc;
+  sc = rtems_task_set_priority( RTEMS_SELF, RTEMS_CURRENT_PRIORITY, &prio );
+  T_rsc_success( sc );
+  T_eq_u32( prio, PRIO_NORMAL );
+
+HigherPriority: |
+  SetSelfPriority( PRIO_HIGH );
+  rtems_task_priority prio;
+  rtems_status_code sc;
+  sc = rtems_task_set_priority( RTEMS_SELF, RTEMS_CURRENT_PRIORITY, &prio );
+  T_rsc_success( sc );
+  T_eq_u32( prio, PRIO_HIGH );
+
+  StartLog: |
+  T_thread_switch_log *log;
+  log = T_thread_switch_record_4( &ctx->thread_switch_log );
+
+CheckPreemption: |
+  log = &ctx->thread_switch_log;
+  T_eq_sz( log->header.recorded, 2 );
+  T_eq_u32( log->events[ 0 ].heir, ctx->runner_id );
+  T_eq_u32( log->events[ 1 ].heir, ctx->worker_id );
+
+CheckNoPreemption: |
+  log = &ctx->thread_switch_log;
+  T_le_sz( log->header.recorded, 1 );
+  for ( size_t i = 0; i < log->header.recorded; ++i ) {
+    T_ne_u32( log->events[ i ].executing, ctx->worker_id );
+    T_eq_u32( log->events[ i ].heir, ctx->runner_id );
+  }
+
+RunnerScheduler: |
+  uint32_t processor = {};
+  rtems_status_code sc1;
+  rtems_id current_sched;
+  sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
+  T_log( T_NORMAL, "current scheduler id: %d", &current_sched);
+  sc1 = rtems_scheduler_ident_by_processor( processor, &ctx->runner_sched );
+  T_rsc_success( sc1 );
+  T_log( T_NORMAL, "runner scheduler id: %d", &ctx->runner_sched);
+  sc1 = rtems_task_set_scheduler(RTEMS_SELF, &ctx->runner_sched, RTEMS_CURRENT_PRIORITY);
+  T_rsc_success( sc1 );
+  sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
+  T_log( T_NORMAL, "current scheduler id: %d", &current_sched);
+
+OtherScheduler: |
+  uint32_t processor = {};
+  rtems_status_code sc1;
+  rtems_id current_sched;
+  sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
+  T_log( T_NORMAL, "current scheduler id: %d", &current_sched);
+  sc1 = rtems_scheduler_ident_by_processor( processor, &ctx->other_sched );
+  T_rsc_success( sc1 );
+  T_log( T_NORMAL, "other scheduler id: %d", &ctx->other_sched);
+  sc1 = rtems_task_set_scheduler(RTEMS_SELF, &ctx->other_sched, RTEMS_CURRENT_PRIORITY);
+  T_rsc_success( sc1 );
+  sc1 = rtems_task_get_scheduler( RTEMS_SELF, current_sched );
+  T_log( T_NORMAL, "current scheduler id: %d", &current_sched);
+
+SetProcessor: |
+  T_eq_u32( rtems_scheduler_get_processor_maximum(), 2 );
+  uint32_t processor = {};
+  cpu_set_t cpuset;
+  CPU_ZERO(&cpuset);
+  CPU_SET(processor, &cpuset);
diff --git a/formal/promela/models/messages/msg-mgr-model-run.h b/formal/promela/models/messages/msg-mgr-model-run.h
new file mode 100644
index 00000000..e9430df1
--- /dev/null
+++ b/formal/promela/models/messages/msg-mgr-model-run.h
@@ -0,0 +1,191 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/*
+static void Worker{0}( rtems_task_argument arg )
+{{
+  Context *ctx;
+
+  ctx = (Context *) arg;
+  rtems_event_set events;
+
+  T_log( T_NORMAL, "Worker Running" );
+  TestSegment4( ctx );
+  T_log( T_NORMAL, "Worker finished" );
+
+  rtems_event_receive( RTEMS_ALL_EVENTS, RTEMS_DEFAULT_OPTIONS, 0, &events );
+}}
+
+
+RTEMS_ALIGNED( RTEMS_TASK_STORAGE_ALIGNMENT ) static char WorkerStorage{0}[
+  RTEMS_TASK_STORAGE_SIZE(
+    MAX_TLS_SIZE + RTEMS_MINIMUM_STACK_SIZE,
+    WORKER_ATTRIBUTES
+  )
+];
+
+static const rtems_task_config WorkerConfig{0} = {{
+  .name = rtems_build_name( 'W', 'O', 'R', 'K' ),
+  .initial_priority = PRIO_LOW,
+  .storage_area = WorkerStorage{0},
+  .storage_size = sizeof( WorkerStorage{0} ),
+  .maximum_thread_local_storage_size = MAX_TLS_SIZE,
+  .initial_modes = RTEMS_DEFAULT_MODES,
+  .attributes = WORKER_ATTRIBUTES
+}};
+
+*/
+static void Worker1( rtems_task_argument arg )
+{{
+  Context *ctx;
+
+  ctx = (Context *) arg;
+  rtems_event_set events;
+
+  T_log( T_NORMAL, "Worker1 Running" );
+  TestSegment4( ctx );
+  T_log( T_NORMAL, "Worker1 finished" );
+
+  rtems_event_receive( RTEMS_ALL_EVENTS, RTEMS_DEFAULT_OPTIONS, 0, &events );
+}}
+
+static void Worker2( rtems_task_argument arg )
+{{
+  Context *ctx;
+
+  ctx = (Context *) arg;
+  rtems_event_set events;
+
+  T_log( T_NORMAL, "Worker2 Running" );
+  TestSegment5( ctx );
+  T_log( T_NORMAL, "Worker2 finished" );
+
+  rtems_event_receive( RTEMS_ALL_EVENTS, RTEMS_DEFAULT_OPTIONS, 0, &events );
+}}
+
+static void RtemsModelMessageMgr_Setup{0}(
+  RtemsModelMessageMgr_Context *ctx
+)
+{{
+  rtems_status_code   sc;
+  rtems_task_priority prio;
+
+  T_log( T_NORMAL, "Runner Setup" );
+
+  memset( ctx, 0, sizeof( *ctx ) );
+  ctx->runner_thread = _Thread_Get_executing();
+  ctx->runner_id = ctx->runner_thread->Object.id;
+  ctx->worker1_wakeup = CreateWakeupSema();
+  ctx->worker2_wakeup = CreateWakeupSema();
+  ctx->runner_wakeup = CreateWakeupSema();
+
+  sc = rtems_task_get_scheduler( RTEMS_SELF, &ctx->runner_sched );
+  T_rsc_success( sc );
+
+  #if defined(RTEMS_SMP)
+  sc = rtems_scheduler_ident_by_processor( 1, &ctx->other_sched );
+  T_rsc_success( sc );
+  T_ne_u32( ctx->runner_sched, ctx->other_sched );
+  #endif
+
+  prio = 0;
+  sc = rtems_task_set_priority( RTEMS_SELF, PRIO_NORMAL, &prio );
+  T_rsc_success( sc );
+  T_eq_u32( prio, PRIO_HIGH );
+
+  //sc = rtems_task_construct( &WorkerConfig{0}, &ctx->worker_id );
+  //T_log( T_NORMAL, "Construct Worker, sc = %x", sc );
+  //T_assert_rsc_success( sc );
+
+  //T_log( T_NORMAL, "Starting Worker..." );
+  //sc = rtems_task_start( ctx->worker_id, Worker{0}, (rtems_task_argument) ctx );
+  //T_log( T_NORMAL, "Started Worker, sc = %x", sc );
+  //T_assert_rsc_success( sc );
+
+  sc = rtems_task_create("WRKR",
+                          PRIO_NORMAL,
+                          RTEMS_MINIMUM_STACK_SIZE,
+                          RTEMS_DEFAULT_MODES,
+                          RTEMS_DEFAULT_ATTRIBUTES,
+                          &ctx->worker1_id);
+  T_assert_rsc_success( sc );
+
+  T_log( T_NORMAL, "Starting Worker1..." );
+  sc = rtems_task_start( ctx->worker1_id, Worker1,ctx );
+  T_log( T_NORMAL, "Started Worker1, sc = %x", sc );
+  T_assert_rsc_success( sc );
+
+  sc = rtems_task_create("WRKR",
+                          PRIO_NORMAL,
+                          RTEMS_MINIMUM_STACK_SIZE,
+                          RTEMS_DEFAULT_MODES,
+                          RTEMS_DEFAULT_ATTRIBUTES,
+                          &ctx->worker2_id);
+  T_assert_rsc_success( sc );
+
+  T_log( T_NORMAL, "Starting Worker2..." );
+  sc = rtems_task_start( ctx->worker2_id, Worker2,ctx );
+  T_log( T_NORMAL, "Started Worker2, sc = %x", sc );
+  T_assert_rsc_success( sc );
+
+}}
+
+
+static void RtemsModelMessageMgr_Setup_Wrap{0}( void *arg )
+{{
+  RtemsModelMessageMgr_Context *ctx;
+
+  ctx = arg;
+  RtemsModelMessageMgr_Setup{0}( ctx );
+}}
+
+
+static RtemsModelMessageMgr_Context RtemsModelMessageMgr_Instance{0};
+
+static T_fixture RtemsModelMessageMgr_Fixture{0} = {{
+  .setup = RtemsModelMessageMgr_Setup_Wrap{0},
+  .stop = NULL,
+  .teardown = RtemsModelMessageMgr_Teardown_Wrap,
+  .scope = RtemsModelMessageMgr_Scope,
+  .initial_context = &RtemsModelMessageMgr_Instance{0}
+}};
+
+static T_fixture_node RtemsModelMessageMgr_Node{0};
+
+void RtemsModelMessageMgr_Run{0}()
+{{
+  RtemsModelMessageMgr_Context *ctx;
+
+  T_set_verbosity( T_NORMAL );
+
+  T_log( T_NORMAL, "Runner Invoked" );
+  T_log( T_NORMAL, "Pushing Test Fixture..." );
+
+
+  ctx = T_push_fixture(
+    &RtemsModelMessageMgr_Node{0},
+    &RtemsModelMessageMgr_Fixture{0}
+  );
+
+  T_log( T_NORMAL, "Test Fixture Pushed" );
+
+
+
+  ctx->this_test_number = {0};
+
+
+  ctx->send_status = RTEMS_INCORRECT_STATE;
+  ctx->receive_option_set = 0;
+  ctx->receive_timeout = RTEMS_NO_TIMEOUT;
+  _Thread_Wait_flags_set( ctx->runner_thread, THREAD_WAIT_CLASS_PERIOD );
+
+  TestSegment0( ctx );
+
+  Runner( ctx );
+
+  RtemsModelMessageMgr_Cleanup( ctx );
+
+  T_log( T_NORMAL, "Run Pop Fixture" );
+  T_pop_fixture();
+}}
+
+/** @}} */
diff --git a/formal/promela/models/messages/msg-mgr-model.pml b/formal/promela/models/messages/msg-mgr-model.pml
new file mode 100644
index 00000000..36c54571
--- /dev/null
+++ b/formal/promela/models/messages/msg-mgr-model.pml
@@ -0,0 +1,842 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+// Message queue attributes
+
+#define TASK_MAX 4 //three rtems tasks
+#define NULL 0
+
+#define SEMA_MAX 3
+
+#define BAD_ID TASK_MAX
+
+#define MAX_MESSAGE_QUEUES 3
+#define MAX_PENDING_MESSAGES 4
+#define MAX_MESSAGE_SIZE 1
+#define QUEUE_NAME 1
+
+//define in cpukit/include/rtems/rtems/status.h
+#define RC_OK      0  // RTEMS_SUCCESSFUL
+#define RC_InvName 3  // RTEMS_INVALID_NAME 
+#define RC_InvId   4  // RTEMS_INVALID_ID
+#define RC_InvAddr 9  // RTEMS_INVALID_ADDRESS
+#define RC_Unsat   13 // RTEMS_UNSATISFIED
+#define RC_Timeout 6  // RTEMS_TIMEOUT
+#define RC_InvSize 8 // RTEMS_INVALID_SIZE
+#define RC_InvNum 10 // RTEMS_INVALID_NUMBER
+#define RC_TooMany 5 // RTEMS_TOO_MANY
+
+inline outputDefines() {
+    printf("@@@ %d DEF TASK_MAX %d\n",_pid,TASK_MAX);
+    printf("@@@ %d DEF BAD_ID %d\n",_pid,BAD_ID);
+    printf("@@@ %d DEF SEMA_MAX %d\n",_pid,SEMA_MAX);
+    printf("@@@ %d DEF MAX_MESSAGE_SIZE %d\n",_pid, MAX_MESSAGE_SIZE);
+    printf("@@@ %d DEF MAX_MESSAGE_QUEUES %d\n",_pid, MAX_MESSAGE_QUEUES);
+    printf("@@@ %d DEF MAX_PENDING_MESSAGES %d\n",_pid, MAX_PENDING_MESSAGES);
+}
+
+
+mtype = {
+  Zombie, Ready, MsgWait, TimeWait, OtherWait, // Task states
+  Wait, NoWait // Option Set values
+};
+
+
+// Tasks
+typedef Task {
+  byte nodeid; // So we can spot remote calls
+  byte pmlid; // Promela process id
+  mtype state ; // {Ready,EventWait,TickWait,OtherWait}
+  bool preemptable ;
+  byte prio ; // lower number is higher priority
+  int ticks; //
+  bool tout; // true if woken by a timeout
+  bool doCreate; // whether to create a queue
+  bool doSend; //whether task should send
+  bool doReceive; //whether task should receive
+  bool doWait; //whether task should wait message
+  int rcvInterval; //how many ticks to wait
+  int rcvMsg; //hold value of message received, modelling receive buffer
+  int sndMsg; //hold value of message to send, modelling send buffer
+  int targetQueue; //queue id for task to interact with
+  int numSends; //number of message send calls to make
+  int msgSize; //size of message to send
+};
+
+Task tasks[TASK_MAX]; // tasks[0] models a NULL dereference
+
+
+byte sendrc;            // Sender global variable
+byte recrc;             // Receiver global variable
+byte qrc              // creation variable
+byte recout[TASK_MAX] ; // models receive 'out' location.
+
+
+bool semaphore[SEMA_MAX]; // Semaphore
+
+mtype = {
+  FIFO, PRIORITY
+};
+
+typedef Config {
+    int name; //An integer is used to represent valid RTEMS_NAME
+    int count; //Max messages for a queue
+    int maxSize; //Max message size
+    mtype attrSet; // RTEMS_ATTRIBUTE_SET, FIFO||priority
+};
+
+typedef MessageQueue {
+  Config config;
+  int messages [MAX_PENDING_MESSAGES] //message circular buffer
+  int head; //top of message queue
+  int tail; //end of message queue
+  bool queueFull; //used to determine full or empty state
+  int waitingTasks [TASK_MAX]; //task circular buffer
+  int nextTask; //top of task queue
+  int lastTask; //end of task queue
+  bool taskFull;
+};
+
+MessageQueue queueList[MAX_MESSAGE_QUEUES]; //queueList[0] is null
+
+/*
+* Helper functions for task
+* and message queue operations
+*/
+
+inline enqueueTask(id, qid) {
+  atomic{
+    queueList[qid].waitingTasks[queueList[qid].lastTask] = id;
+    if 
+    :: queueList[qid].lastTask == TASK_MAX-1 -> queueList[qid].lastTask = 0;
+    :: else -> queueList[qid].lastTask++;
+    fi
+    if
+    :: queueList[qid].lastTask == queueList[qid].nextTask -> queueList[qid].taskFull = true;
+    :: else -> skip;
+    fi
+  }
+}
+
+inline dequeueTask(id,qid) {
+  atomic{
+    id = queueList[qid].waitingTasks[queueList[qid].nextTask];
+    if 
+    :: queueList[qid].nextTask == TASK_MAX-1 -> queueList[qid].nextTask = 0;
+    :: else -> queueList[qid].nextTask++;
+    fi
+    if
+    :: queueList[qid].lastTask == queueList[qid].nextTask -> queueList[qid].taskFull = false;
+    :: else -> skip;
+    fi
+  }
+}
+
+
+
+inline enqueueMessage(id,msg) {
+  atomic{
+    queueList[id].messages[queueList[id].head] = msg;
+   //printf("enqueue message %d", msg);
+    if 
+    :: queueList[id].head == MAX_PENDING_MESSAGES-1 -> queueList[id].head = 0;
+    :: else -> queueList[id].head++;
+    fi
+    if
+    :: queueList[id].head == queueList[id].tail -> queueList[id].queueFull = true;
+    :: else -> skip;
+    fi
+  }
+}
+
+inline dequeueMessage(id,msg) {
+  atomic{
+    msg = queueList[id].messages[queueList[id].tail];
+    //printf("dequeue message %d", msg);
+    if 
+    :: msg == 0 -> skip;
+    :: queueList[id].tail == MAX_PENDING_MESSAGES-1 -> queueList[id].tail = 0;
+    :: else -> queueList[id].tail++;
+    fi
+    if
+    :: queueList[id].head == queueList[id].tail -> queueList[id].queueFull = false;
+    :: else -> skip;
+    fi
+  }
+}
+
+
+inline sizeOfQueue(id, qsize) {
+  atomic{
+  if 
+  :: queueList[id].head == queueList[id].tail ->
+      if
+      ::  -> qsize = MAX_PENDING_MESSAGES;
+      :: else -> qsize = 0;
+      fi
+  :: queueList[id].head > queueList[id].tail -> qsize = queueList[id].head - queueList[id].tail;
+  :: queueList[id].head < queueList[id].tail -> qsize = MAX_PENDING_MESSAGES + queueList[id].head - queueList[id].tail;
+  fi
+  return qsize;
+  }
+}
+
+//Declare needed arrays, variables
+inline outputDeclarations () {
+  printf("@@@ %d DECL byte sendrc 0\n",_pid);
+  printf("@@@ %d DECL byte recrc 0\n",_pid);
+  printf("@@@ %d DECL byte qrc 0\n",_pid);
+  printf("@@@ %d DECL uint8_t send_counter 0\n",_pid);
+  printf("@@@ %d DCLARRAY uint8_t receive_buffer MAX_MESSAGE_SIZE\n",_pid);
+  printf("@@@ %d DCLARRAY uint8_t send_buffer MAX_MESSAGE_SIZE\n",_pid);
+  printf("@@@ %d DCLARRAY RTEMS_MESSAGE_QUEUE_BUFFER queue_buffer MAX_PENDING_MESSAGES\n",_pid);
+  // Rather than refine an entire Task array, we refine array 'slices'
+  printf("@@@ %d DCLARRAY byte recout TASK_MAX\n",_pid);
+  printf("@@@ %d DCLARRAY Semaphore semaphore SEMA_MAX\n",_pid);
+}
+
+inline nl() { printf("\n") }
+/*
+ * Synchronisation Mechanisms
+ *  Obtain(sem_id)   - call that waits to obtain semaphore `sem_id`
+ *  Release(sem_id)  - call that releases semaphore `sem_id`
+ *  Released(sem_id) - simulates ecosystem behaviour releases `sem_id`
+ *
+ * Binary semaphores:  True means available, False means in use.
+ */
+inline Obtain(sem_id){
+  atomic{
+    printf("@@@ %d WAIT %d\n",_pid,sem_id);
+    semaphore[sem_id] ;        // wait until available
+    semaphore[sem_id] = false; // set as in use
+    printf("@@@ %d LOG WAIT %d Over\n",_pid,sem_id);
+  }
+}
+
+inline Release(sem_id){
+  atomic{
+    printf("@@@ %d SIGNAL %d\n",_pid,sem_id);
+    semaphore[sem_id] = true ; // release
+  }
+}
+
+inline Released(sem_id)
+{
+  semaphore[sem_id] = true ;
+}
+
+
+/*
+ * waitUntilReady(id) logs that task[id] is waiting,
+ * and then attempts to execute a statement that blocks,
+ * until some other process changes task[id]'s state to Ready.
+ * It relies on the fact that if a statement blocks inside an atomic block,
+ * the block loses its atomic behaviour and yields to other Promela processes
+ *
+ * It is used to model a task that has been suspended for any reason.
+ */
+inline waitUntilReady(id){
+  atomic{
+    printf("@@@ %d LOG Task %d waiting, state = ",_pid,id);
+    printm(tasks[id].state); nl()
+  }
+  tasks[id].state == Ready; // breaks out of atomics if false
+  printf("@@@ %d STATE %d Ready\n",_pid,id)
+}
+
+
+/* message_queue_create()
+* creates a message queue object from passed parameters
+* queue_name -rtems object name
+* msg_count - max messages in queue
+* max_size - max message size
+* rc - return flag
+*/
+
+inline message_queue_create(queue_name, msg_count, max_size, rc) {
+    atomic{
+      //only one queue created
+      int qid = 1;
+      if
+      ::  queue_name == 0 -> rc = RC_InvName;
+      ::  max_size == 0 -> rc = RC_InvSize;
+      ::  msg_count == 0 -> rc = RC_InvNum;
+      ::  else -> 
+            queueList[qid].config.count = msg_count;
+            queueList[qid].config.maxSize = max_size;
+            queueList[qid].queueFull = false;
+            queueList[qid].config.name = queue_name;
+            rc = RC_OK;
+      fi
+      ;
+  }
+}
+
+
+/*
+* message_queue_send
+*    self: id of calling task
+*    qid: id of queue
+*    msg : message
+*    size : size of the message
+*    rc: return code
+*
+* This directive will send a message to the to the specficied
+* message queue.
+*  If there is a task waiting it will copy the message to that tasks
+*  buffer and unblock it
+*  If there is no task waiting it will ad the message to the message queue
+*/
+
+inline message_queue_send(self,qid,msg,size,rc) {
+    atomic{
+      int queuedTask = queueList[qid].waitingTasks[queueList[qid].nextTask];
+      if
+      ::  qid == 0 -> rc = RC_InvId;
+      ::  else ->
+          if
+          ::  msg == NULL -> rc = RC_InvAddr;
+          ::  size > queueList[qid].config.maxSize -> rc = RC_InvSize;
+          ::  queueList[qid].queueFull -> rc = RC_TooMany;
+          ::  else ->
+              if 
+              ::  queuedTask == 0 -> //no task waiting, add to buffer
+                  enqueueMessage(qid,msg);
+                  printf("@@@ %d LOG Send queueing message\n",_pid)
+                  rc = RC_OK;
+              ::  else -> //task waiting
+                  dequeueTask(queuedTask,qid);
+                  enqueueMessage(qid,msg);
+                  printf("@@@ %d LOG Send to task %d\n",_pid, queuedTask)
+                  //tasks[queuedTask].rcvMsg = msg;
+                  //printf("%d rcv msg %d",_pid,tasks[queuedTask].rcvMsg)
+                  tasks[queuedTask].state = Ready
+                  printf("@@@ %d STATE %d Ready\n",_pid, queuedTask)
+                  rc = RC_OK;
+              fi
+          fi
+      fi 
+    }
+}
+
+inline message_queue_receive(self,qid,msg,rc) { 
+  int rcvmsg;
+  atomic{
+    if
+    :: qid == 0 -> rc = RC_InvId;
+    //:: msg == 0 -> rc = RC_InvAddr
+    //:: size >= config.maxSize -> RC_InvSize
+    :: else -> 
+      dequeueMessage(qid,msg);
+      if
+      :: msg == 0 && !tasks[self].doWait -> 
+        rc = RC_Unsat; printf("@@@ %d LOG Receive Not Satisfied (no wait)\n",_pid)
+      :: msg == 0 && tasks[self].doWait ->
+        printf("@@@ %d LOG Receive Not Satisfied (timeout %d)\n",
+                _pid,
+                tasks[self].rcvInterval);
+        tasks[self].ticks = tasks[self].rcvInterval;
+        tasks[self].tout = false;
+        printf("@@@ %d STATE %d TimeWait %d\n",
+                _pid,
+                self,
+                tasks[self].rcvInterval);
+        tasks[self].state = TimeWait;
+        enqueueTask(self,qid);
+        waitUntilReady(self);
+        
+        if
+        ::  tasks[self].tout  ->  dequeueTask(self,qid); rc = RC_Timeout; 
+        ::  else              -> dequeueMessage(qid,msg);
+        fi
+
+      :: else -> rc = RC_OK;
+      fi
+    fi   
+  }
+}
+
+
+/*
+ * Model Processes
+ * We shall use four processes in this model.
+ *  One will represent the RTEMS send task 
+ *  Two will represent the RTEMS receive tasks
+ *  One will model a timer
+ */
+
+// These are not output to test generation
+#define SEND_ID 1
+#define RCV1_ID 2
+#define RCV2_ID 3
+
+/*
+ * Sender Scenario
+ */
+byte sendTarget;
+byte msize;
+bool sendAgain
+int totalSendCount
+int currSendCount
+/*
+ * Receiver Scenario
+ */
+
+/*
+ * Semaphore Setup
+ */
+int sendSema;
+int rcvSema1;
+int startSema;
+int rcvSema2;
+
+/*
+* Queue setup
+*
+*/
+bool queueCreated;
+int queueId;
+
+
+
+
+mtype = {Send,Receive,SndRcv, RcvSnd};
+mtype scenario;
+
+inline chooseScenario() {
+
+  sendAgain = false;
+  semaphore[0] = false;
+  semaphore[1] = false;
+  semaphore[2] = false;
+  sendSema = 0;
+  rcvSema1 = 1;
+  rcvSema2 = 2;
+  startSema = sendSema;
+  tasks[SEND_ID].doCreate = true;
+
+  //Queue parameters
+  queueCreated = false;
+  queueId = 1;
+
+  msize = MAX_MESSAGE_SIZE;
+  //set up defaults
+  tasks[SEND_ID].numSends = 1;
+  tasks[SEND_ID].sndMsg = 1;
+  tasks[SEND_ID].targetQueue = queueId;
+  tasks[RCV1_ID].targetQueue = queueId;
+  tasks[RCV2_ID].targetQueue = queueId;
+  tasks[SEND_ID].sndMsg = 1;
+  tasks[SEND_ID].msgSize = MAX_MESSAGE_SIZE;
+
+
+  //select scenario
+  if
+  ::  scenario = Send;
+  ::  scenario = Receive;
+  ::  scenario = SndRcv;
+  ::  scenario = RcvSnd;
+  fi
+
+  atomic{printf("@@@ %d LOG scenario ",_pid); 
+  printm(scenario); 
+  nl()};
+
+
+  if
+  :: scenario == Send ->
+        tasks[RCV1_ID].doReceive = false;
+        tasks[RCV2_ID].doReceive = false;
+        tasks[SEND_ID].doSend = true;
+        if
+        ::  tasks[SEND_ID].targetQueue = 0;
+            printf("@@@ %d LOG sub-scenario Send Bad ID\n", _pid)
+        ::  tasks[SEND_ID].targetQueue = queueId;
+            printf("@@@ %d LOG sub-scenario Send Success\n", _pid)
+        ::  tasks[SEND_ID].msgSize = MAX_MESSAGE_SIZE + 1;
+            printf("@@@ %d LOG sub-scenario Send Size Error\n", _pid)
+        ::  tasks[SEND_ID].sndMsg = 0;
+            printf("@@@ %d LOG sub-scenario Buffer Address Error\n", _pid)
+        ::  tasks[SEND_ID].numSends = MAX_PENDING_MESSAGES + 1;
+            printf("@@@ %d LOG sub-scenario Too Many messages Error\n", _pid)         
+        fi
+
+  :: scenario == Receive ->
+        tasks[SEND_ID].doSend = false;
+        tasks[RCV1_ID].doReceive = true;
+        tasks[RCV2_ID].doReceive = false;
+        startSema = rcvSema1;
+        
+        if
+        ::  tasks[RCV1_ID].doWait = false;
+            if
+            ::  tasks[RCV1_ID].targetQueue = 0;
+                printf("@@@ %d LOG sub-scenario Rcv Bad ID No Wait\n", _pid)
+            ::  tasks[SEND_ID].targetQueue = queueId;
+                printf("@@@ %d LOG sub-scenario Rcv Success No Wait\n", _pid, tasks[RCV1_ID].doWait, tasks[RCV1_ID].rcvInterval)
+            fi 
+        ::  tasks[RCV1_ID].doWait = true; tasks[RCV1_ID].rcvInterval = 5;
+            printf("@@@ %d LOG sub-scenario Rcv Success wait:%d interval:%d\n", _pid, tasks[RCV1_ID].doWait, tasks[RCV1_ID].rcvInterval)
+        fi
+        
+        /*
+        if
+        ::  tasks[RCV2_ID].doWait = false;  
+        ::  tasks[RCV2_ID].doWait = true; tasks[RCV2_ID].rcvInterval = 5;
+        fi
+        printf("@@@ %d LOG sub-scenario Receive2 wait:%d interval:%d\n", _pid, tasks[RCV2_ID].doWait, tasks[RCV2_ID].rcvInterval)
+        */
+
+  :: scenario == SndRcv ->
+
+        if
+        ::  tasks[SEND_ID].numSends = 2;     
+        ::  tasks[SEND_ID].numSends = 1;
+        fi
+        printf("@@@ %d LOG sub-scenario SndRcv numSends:%d\n", 
+                _pid, 
+                tasks[SEND_ID].numSends
+                )
+        /* 
+        if
+        ::  tasks[RCV1_ID].doWait = false;      
+        ::  tasks[RCV1_ID].doWait = true; tasks[RCV1_ID].rcvInterval = 5;
+        fi
+        printf("@@@ %d LOG sub-scenario Receive1 wait:%d interval:%d\n", _pid, tasks[RCV1_ID].doWait, tasks[RCV1_ID].rcvInterval)
+        if
+        ::  tasks[RCV2_ID].doWait = false;      
+        ::  tasks[RCV2_ID].doWait = true; tasks[RCV2_ID].rcvInterval = 5;
+        fi
+        printf("@@@ %d LOG sub-scenario Receive2 wait:%d interval:%d\n", _pid, tasks[RCV2_ID].doWait, tasks[RCV2_ID].rcvInterval)
+        */
+        
+        tasks[SEND_ID].doSend = true;
+        tasks[RCV1_ID].doReceive = true;
+        tasks[RCV2_ID].doReceive = true;
+
+  :: scenario == RcvSnd ->
+        startSema = rcvSema1;
+        tasks[SEND_ID].doSend = true;
+        tasks[RCV1_ID].doReceive = true;
+        tasks[RCV2_ID].doReceive = false;
+        tasks[RCV1_ID].doWait = true;  tasks[RCV1_ID].rcvInterval = 10;
+        //tasks[SEND_ID].numSends = 2
+        /*
+        if
+        :: tasks[RCV1_ID].doWait = false; tasks[RCV2_ID].doWait = false;
+        :: tasks[RCV1_ID].doWait = true;  tasks[RCV2_ID].doWait = true; tasks[RCV1_ID].rcvInterval = 10; tasks[RCV2_ID].rcvInterval = 10;
+        fi
+        printf("@@@ %d LOG sub-scenario RcvSnd wait:%d interval:%d\n", _pid, tasks[RCV1_ID].doWait, tasks[RCV1_ID].rcvInterval)
+        */
+
+  fi
+}
+
+
+proctype Sender (byte taskid) {
+
+  tasks[taskid].pmlid = _pid;
+  tasks[taskid].state = Ready;
+  printf("@@@ %d TASK Runner\n",_pid,taskid);
+  
+  if 
+  ::  (tasks[taskid].doCreate && !queueCreated) ->
+      printf("@@@ %d CALL message_queue_construct %d %d %d %d %d qrc\n", _pid, 
+              taskid, 
+              QUEUE_NAME,
+              MAX_PENDING_MESSAGES, 
+              MAX_MESSAGE_SIZE, 
+              queueId);
+      message_queue_create(QUEUE_NAME, 
+                            MAX_PENDING_MESSAGES, 
+                            MAX_MESSAGE_SIZE, 
+                            qrc);
+      printf("@@@ %d SCALAR qrc %d\n",_pid,qrc);
+      queueCreated = true;
+      Release(startSema);
+  fi
+  
+  if
+  :: tasks[taskid].doSend -> 
+      Obtain(sendSema);
+      repeat:
+      atomic{
+      printf("@@@ %d CALL message_queue_send %d %d %d %d sendrc\n",
+              _pid,
+              taskid, 
+              tasks[taskid].targetQueue, 
+              tasks[taskid].sndMsg, 
+              tasks[taskid].msgSize);
+      message_queue_send(taskid,
+                          tasks[taskid].targetQueue,
+                          tasks[taskid].sndMsg,
+                          tasks[taskid].msgSize,
+                          sendrc);
+      printf("@@@ %d SCALAR sendrc %d\n",_pid,sendrc);
+      tasks[taskid].numSends-- ;
+      if
+      :: tasks[taskid].numSends != 0 -> tasks[SEND_ID].sndMsg++; goto repeat; 
+      :: scenario == RcvSnd -> skip;
+      :: else -> Release(rcvSema1);
+      fi
+      }
+  :: else -> skip;
+  fi
+
+
+  //adjust semaphore behaviour for RcvSnd as Receive1 starts
+  if 
+  :: scenario == RcvSnd -> 
+        Obtain(rcvSema1);
+        Obtain(rcvSema2);
+  :: else ->         
+        Obtain(sendSema);
+        Obtain(rcvSema2);
+        Obtain(rcvSema1);
+  fi
+  
+  printf("@@@ %d LOG Sender %d finished\n",_pid,taskid);
+  tasks[taskid].state = Zombie;
+  printf("@@@ %d STATE %d Zombie\n",_pid,taskid);
+}
+
+proctype Receiver1 (byte taskid) {
+
+  tasks[taskid].pmlid = _pid;
+  tasks[taskid].state = Ready;
+  printf("@@@ %d TASK Worker1\n",_pid);
+
+  
+  Obtain(rcvSema1);
+
+  if
+  :: tasks[taskid].doReceive && scenario != RcvSnd->
+      atomic{
+      printf("@@@ %d CALL message_queue_receive %d %d %d %d recrc\n",
+              _pid,taskid,
+              tasks[taskid].targetQueue,
+              tasks[taskid].doWait,
+              tasks[taskid].rcvInterval);
+      message_queue_receive(taskid,
+                              tasks[taskid].targetQueue,
+                              tasks[taskid].rcvMsg,
+                              recrc);
+      printf("@@@ %d LOG received %d\n", _pid,tasks[taskid].rcvMsg);
+      printf("@@@ %d SCALAR recrc %d\n",_pid,recrc);
+      Release(rcvSema2);
+      }   
+  :: tasks[taskid].doReceive && scenario == RcvSnd->
+      atomic{
+      Release(sendSema);
+      printf("@@@ %d CALL message_queue_receive %d %d %d %d recrc\n",
+                _pid,
+                taskid,
+                tasks[taskid].targetQueue,
+                tasks[taskid].doWait,
+                tasks[taskid].rcvInterval);
+      message_queue_receive(taskid,
+                              tasks[taskid].targetQueue,
+                              tasks[taskid].rcvMsg,
+                              recrc);
+      printf("@@@ %d LOG received %d\n", _pid,tasks[taskid].rcvMsg);
+      printf("@@@ %d SCALAR recrc %d\n",_pid,recrc);
+      }
+  :: else -> Release(rcvSema2); 
+  fi
+
+ 
+
+  atomic{
+  Release(rcvSema1);
+  printf("@@@ %d LOG Receiver1 %d finished\n",_pid,taskid);
+  tasks[taskid].state = Zombie;
+  printf("@@@ %d STATE %d Zombie\n",_pid,taskid)
+  }
+}
+
+proctype Receiver2 (byte taskid) {
+
+  tasks[taskid].pmlid = _pid;
+  tasks[taskid].state = Ready;
+  printf("@@@ %d TASK Worker2\n",_pid);
+  
+  if
+  :: scenario == RcvSnd ->
+      goto rcvSkip;
+  :: else -> Obtain(rcvSema2);
+  fi
+  
+  
+  if
+  :: tasks[taskid].doReceive && scenario != RcvSnd-> 
+      atomic{
+      printf("@@@ %d CALL message_queue_receive %d %d %d %d recrc\n",
+              _pid,
+              taskid,
+              tasks[taskid].targetQueue,
+              tasks[taskid].doWait,
+              tasks[taskid].rcvInterval);
+      message_queue_receive(taskid,tasks[taskid].targetQueue,tasks[taskid].rcvMsg,recrc);
+      printf("@@@ %d LOG received %d\n", _pid,tasks[taskid].rcvMsg);
+      printf("@@@ %d SCALAR recrc %d\n",_pid,recrc);
+      Release(sendSema);
+      }
+  :: tasks[taskid].doReceive && scenario == RcvSnd->
+      atomic{
+      printf("@@@ %d CALL message_queue_receive %d %d %d %d recrc\n",
+              _pid,
+              taskid,tasks[taskid].targetQueue,
+              tasks[taskid].doWait,
+              tasks[taskid].rcvInterval);
+      Release(sendSema);
+      message_queue_receive(taskid,tasks[taskid].targetQueue,tasks[taskid].rcvMsg,recrc);
+      printf("@@@ %d LOG received %d\n", _pid,tasks[taskid].rcvMsg);
+      printf("@@@ %d SCALAR recrc %d\n",_pid,recrc);
+      }
+  :: else -> Release(sendSema);
+  fi
+
+  rcvSkip:
+  atomic{
+  Release(rcvSema2);
+  printf("@@@ %d LOG Receiver2 %d finished\n",_pid,taskid);
+  tasks[taskid].state = Zombie;
+  printf("@@@ %d STATE %d Zombie\n",_pid,taskid)
+  }
+}
+
+
+/*
+ * We need a process that periodically wakes up blocked processes.
+ * This is modelling background behaviour of the system,
+ * such as ISRs and scheduling.
+ * We visit all tasks in round-robin order (to prevent starvation)
+ * and make them ready if waiting on "other" things.
+ * Tasks waiting for events or timeouts are not touched
+ * This terminates when all tasks are zombies.
+ */
+
+bool stopclock = false;
+
+proctype System () {
+  byte taskid ;
+  bool liveSeen;
+
+  printf("@@@ %d LOG System running...\n",_pid);
+
+  loop:
+  taskid = 1;
+  liveSeen = false;
+
+  printf("@@@ %d LOG Loop through tasks...\n",_pid);
+  atomic {
+    printf("@@@ %d LOG Scenario is ",_pid);
+    printm(scenario); nl();
+  }
+  do   // while taskid < TASK_MAX ....
+  ::  taskid == TASK_MAX -> break;
+  ::  else ->
+      atomic {
+        printf("@@@ %d LOG Task %d state is ",_pid,taskid);
+        printm(tasks[taskid].state); nl()
+      }
+      if
+      :: tasks[taskid].state == Zombie -> taskid++
+      :: else ->
+         if
+         ::  tasks[taskid].state == OtherWait
+             -> tasks[taskid].state = Ready
+                printf("@@@ %d STATE %d Ready\n",_pid,taskid)
+         ::  else -> skip
+         fi
+         liveSeen = true;
+         taskid++
+      fi
+  od
+
+  printf("@@@ %d LOG ...all visited, live:%d\n",_pid,liveSeen);
+
+  if
+  ::  liveSeen -> goto loop
+  ::  else
+  fi
+  printf("@@@ %d LOG All are Zombies, game over.\n",_pid);
+  stopclock = true;
+}
+
+
+/*
+ * We need a process that handles a clock tick,
+ * by decrementing the tick count for tasks waiting on a timeout.
+ * Such a task whose ticks become zero is then made Ready,
+ * and its timer status is flagged as a timeout
+ * This terminates when all tasks are zombies
+ * (as signalled by System via `stopclock`).
+ */
+proctype Clock () {
+  int tid, tix;
+  printf("@@@ %d LOG Clock Started\n",_pid)
+  do
+  ::  stopclock  -> goto stopped
+  ::  !stopclock ->
+      printf(" (tick) \n");
+      tid = 1;
+      do
+      ::  tid == TASK_MAX -> break
+      ::  else ->
+          atomic{printf("Clock: tid=%d, state=",tid); printm(tasks[tid].state); nl()};
+          if
+          ::  tasks[tid].state == TimeWait ->
+              tix = tasks[tid].ticks - 1;
+              // printf("Clock: ticks=%d, tix=%d\n",tasks[tid].ticks,tix);
+              if
+              ::  tix == 0
+                  tasks[tid].tout = true
+                  tasks[tid].state = Ready
+                  printf("@@@ %d STATE %d Ready\n",_pid,tid)
+              ::  else
+                  tasks[tid].ticks = tix
+              fi
+          ::  else // state != TimeWait
+          fi
+          tid = tid + 1
+      od
+  od
+stopped:
+  printf("@@@ %d LOG Clock Stopped\n",_pid);
+}
+
+
+
+init {
+  pid nr;
+
+  printf("Message Manager Model running.\n");
+  printf("Setup...\n");
+  
+  printf("@@@ %d NAME Message_Manager_TestGen\n",_pid)
+  //#define required in test file
+  outputDefines();
+  //Structures and data types required in test file
+  outputDeclarations();
+
+  printf("@@@ %d INIT\n",_pid);
+  chooseScenario();
+
+  printf("Run...\n");
+  //start nececssary processes
+  run System();
+  run Clock();
+  
+  run Sender(SEND_ID);
+  run Receiver1(RCV1_ID);
+  run Receiver2(RCV2_ID);
+  
+  _nr_pr == 1;
+
+#ifdef TEST_GEN
+  assert(false);
+#endif
+
+
+printf("Message Manager Model finished !\n")
+}
\ No newline at end of file
diff --git a/formal/promela/models/messages/tc-msg-mgr-model.c b/formal/promela/models/messages/tc-msg-mgr-model.c
new file mode 100644
index 00000000..cb3176f1
--- /dev/null
+++ b/formal/promela/models/messages/tc-msg-mgr-model.c
@@ -0,0 +1,211 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * @file
+ *
+ * @ingroup RTEMSTestCaseRtemsMessageVal
+ */
+
+/*
+ * Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ */
+
+/*
+ * Do not manually edit this file.  It is part of the RTEMS quality process
+ * and was automatically generated.
+ *
+ * If you find something that needs to be fixed or worded better please
+ * post a report to an RTEMS mailing list or raise a bug report:
+ *
+ * https://docs.rtems.org/branches/master/user/support/bugs.html
+ *
+ * For information on updating and regenerating please refer to:
+ *
+ * https://docs.rtems.org/branches/master/eng/req/howto.html
+ */
+
+#ifdef HAVE_CONFIG_H
+#include "config.h"
+#endif
+
+#include <rtems/rtems/eventimpl.h>
+#include <rtems/rtems/tasksdata.h>
+#include <rtems/score/statesimpl.h>
+#include <rtems/score/threadimpl.h>
+
+#include "tr-msg-mgr-model.h"
+
+#include <rtems/test.h>
+
+
+
+/**
+ * @defgroup RTEMSTestCaseRtemsMessageVal
+ *
+ * @ingroup RTEMSTestSuiteTestsuitesValidation0
+ *
+ * @brief Tests the rtems_message_queue_create, rtems_message_queue_send, 
+ * rtems_message_queue_recieve, rtems_message_queue_delete, rtems_message_queue_ident
+ *
+ * This test case performs the following actions:
+ *
+ * - Runs tests for message manager
+ *
+ * @{
+ */
+
+/**
+ * @fn void T_case_body_RtemsMessageVal( void )
+ */
+
+T_TEST_CASE( RtemsModelMessageMgr0 )
+{
+  RtemsModelMessageMgr_Run0();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr1 )
+{
+  RtemsModelMessageMgr_Run1();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr2 )
+{
+  RtemsModelMessageMgr_Run2();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr3 )
+{
+  RtemsModelMessageMgr_Run3();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr4 )
+{
+  RtemsModelMessageMgr_Run4();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr5 )
+{
+  RtemsModelMessageMgr_Run5();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr6 )
+{
+  RtemsModelMessageMgr_Run6();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr7 )
+{
+  RtemsModelMessageMgr_Run7();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr8 )
+{
+  RtemsModelMessageMgr_Run8();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr9 )
+{
+  RtemsModelMessageMgr_Run9();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr10 )
+{
+  RtemsModelMessageMgr_Run10();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr11 )
+{
+  RtemsModelMessageMgr_Run11();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr12 )
+{
+  RtemsModelMessageMgr_Run12();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr13 )
+{
+  RtemsModelMessageMgr_Run13();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr14 )
+{
+  RtemsModelMessageMgr_Run14();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr15 )
+{
+  RtemsModelMessageMgr_Run15();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr16 )
+{
+  RtemsModelMessageMgr_Run16();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr17 )
+{
+  RtemsModelMessageMgr_Run17();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr18 )
+{
+  RtemsModelMessageMgr_Run18();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr19 )
+{
+  RtemsModelMessageMgr_Run19();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr20 )
+{
+  RtemsModelMessageMgr_Run20();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr21 )
+{
+  RtemsModelMessageMgr_Run21();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr22 )
+{
+  RtemsModelMessageMgr_Run22();
+}
+/*
+T_TEST_CASE( RtemsModelMessageMgr23 )
+{
+  RtemsModelMessageMgr_Run23();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr24 )
+{
+  RtemsModelMessageMgr_Run24();
+}
+
+T_TEST_CASE( RtemsModelMessageMgr25 )
+{
+  RtemsModelMessageMgr_Run25();
+}
+*/
\ No newline at end of file
diff --git a/formal/promela/models/messages/tr-msg-mgr-model.c b/formal/promela/models/messages/tr-msg-mgr-model.c
new file mode 100644
index 00000000..79562e9b
--- /dev/null
+++ b/formal/promela/models/messages/tr-msg-mgr-model.c
@@ -0,0 +1,240 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * @file
+ *
+ * @ingroup RTEMSTestCaseRtemsModelMsgMgr
+ */
+
+/*
+ * Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+ *                    Trinity College Dublin (http://www.tcd.ie)
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ *    notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ *    notice, this list of conditions and the following disclaimer in the
+ *    documentation and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ */
+
+/*
+ * This file was automatically generated.  Do not edit it manually.
+ * Please have a look at
+ *
+ * https://docs.rtems.org/branches/master/eng/req/howto.html
+ *
+ * for information how to maintain and re-generate this file.
+ */
+
+#ifdef HAVE_CONFIG_H
+#include "config.h"
+#endif
+
+#include <rtems/score/threadimpl.h>
+
+#include "tr-msg-mgr-model.h"
+
+static const char PromelaModelMessageMgr[] = "/PML-MessageMgr";
+
+rtems_id CreateWakeupSema( void )
+{
+  rtems_status_code sc;
+  rtems_id id;
+
+  sc = rtems_semaphore_create(
+    rtems_build_name( 'W', 'K', 'U', 'P' ),
+    0,
+    RTEMS_SIMPLE_BINARY_SEMAPHORE,
+    0,
+    &id
+  );
+  T_assert_rsc_success( sc );
+
+  return id;
+}
+
+void DeleteWakeupSema( rtems_id id )
+{
+  if ( id != 0 ) {
+    rtems_status_code sc;
+
+    sc = rtems_semaphore_delete( id );
+    T_rsc_success( sc );
+  }
+}
+
+void Wait( rtems_id id )
+{
+  rtems_status_code sc;
+
+  sc = rtems_semaphore_obtain( id, RTEMS_WAIT, RTEMS_NO_TIMEOUT );
+  T_quiet_rsc_success( sc );
+}
+
+void Wakeup( rtems_id id )
+{
+  rtems_status_code sc;
+
+  sc = rtems_semaphore_release( id );
+  T_quiet_rsc_success( sc );
+}
+
+rtems_option mergeopts( bool wait )
+{
+  rtems_option opts;
+
+  if ( wait ) { opts = RTEMS_WAIT; }
+  else { opts = RTEMS_NO_WAIT; } ;
+  return opts;
+}
+
+rtems_interval getTimeout( int timeout )
+{
+  rtems_interval tout;
+
+  if ( timeout == 0 ) { tout = RTEMS_NO_TIMEOUT; }
+  else { tout = timeout; } ;
+  return tout;
+}
+
+rtems_id idNull( Context *ctx, bool passedid )
+{
+  rtems_id id;
+
+  if ( passedid ) { return ctx->queue_id; }
+  else { return NULL; }
+}
+
+void checkTaskIs( rtems_id expected_id )
+{
+  rtems_id own_id;
+
+  own_id = _Thread_Get_executing()->Object.id;
+  T_eq_u32( own_id, expected_id );
+}
+
+void initialise_pending( rtems_event_set pending[], int max )
+{
+  int i;
+
+  for( i=0; i < max; i++ ) {
+    pending[i] = 0;
+  }
+}
+
+void initialise_semaphore( Context *ctx, rtems_id semaphore[] )
+{
+  semaphore[0] = ctx->runner_wakeup;
+  semaphore[1] = ctx->worker1_wakeup;
+  semaphore[2] = ctx->worker2_wakeup;
+}
+
+void ShowWorkerSemaId( Context *ctx ) {
+  T_printf( "L:ctx->worker1_wakeup = %d\n", ctx->worker1_wakeup );
+  T_printf( "L:ctx->worker2_wakeup = %d\n", ctx->worker2_wakeup );
+}
+
+void ShowRunnerSemaId( Context *ctx ) {
+  T_printf( "L:ctx->runner_wakeup = %d\n", ctx->runner_wakeup );
+}
+
+static void RtemsModelMessageMgr_Teardown(
+  RtemsModelMessageMgr_Context *ctx
+)
+{
+  rtems_status_code   sc;
+  rtems_task_priority prio;
+
+  T_log( T_NORMAL, "Runner Teardown" );
+
+  prio = 0;
+  sc = rtems_task_set_priority( RTEMS_SELF, PRIO_HIGH, &prio );
+  T_rsc_success( sc );
+  T_eq_u32( prio, PRIO_NORMAL );
+
+  if ( ctx->worker1_id != 0 ) {
+    T_printf( "L:Deleting Task id : %d\n", ctx->worker1_id );
+    sc = rtems_task_delete( ctx->worker1_id );
+    T_rsc_success( sc );
+  }
+
+  T_log( T_NORMAL, "Deleting Worker1 Wakeup Semaphore" );
+  DeleteWakeupSema( ctx->worker1_wakeup );
+
+
+  if ( ctx->worker2_id != 0 ) {
+    T_printf( "L:Deleting Task id : %d\n", ctx->worker2_id );
+    sc = rtems_task_delete( ctx->worker2_id );
+    T_rsc_success( sc );
+  }
+
+  T_log( T_NORMAL, "Deleting Worker2 Wakeup Semaphore" );
+  DeleteWakeupSema( ctx->worker2_wakeup );
+
+  T_log( T_NORMAL, "Deleting Runner Wakeup Semaphore" );
+  DeleteWakeupSema( ctx->runner_wakeup );
+}
+
+void RtemsModelMessageMgr_Teardown_Wrap( void *arg )
+{
+  RtemsModelMessageMgr_Context *ctx;
+
+  ctx = arg;
+  RtemsModelMessageMgr_Teardown( ctx );
+}
+
+
+size_t RtemsModelMessageMgr_Scope( void *arg, char *buf, size_t n )
+{
+  RtemsModelMessageMgr_Context *ctx;
+  size_t m;
+  int p10;
+  int tnum ;
+  char digit;
+
+  ctx = arg;
+  p10 = POWER_OF_10;
+
+  m = T_str_copy(buf, PromelaModelMessageMgr, n);
+  buf += m;
+  tnum = ctx->this_test_number;
+  while( p10 > 0 && m < n )
+  {
+    digit = (char) ( (int) '0' + tnum / p10 );
+    buf[0] = digit;
+    ++buf;
+    ++m;
+    tnum = tnum % p10;
+    p10 /= 10;
+  }
+  return m;
+}
+
+void RtemsModelMessageMgr_Cleanup(
+  RtemsModelMessageMgr_Context *ctx
+)
+{
+  rtems_status_code status;
+
+  if (ctx->queue_id != 0){
+    status = rtems_message_queue_delete(ctx->queue_id);
+    if (status != RTEMS_SUCCESSFUL) { T_quiet_rsc( status, RTEMS_INVALID_ID ); }
+    else { T_rsc_success( status ); }
+    ctx->queue_id = RTEMS_ID_NONE;
+  }
+}
diff --git a/formal/promela/models/messages/tr-msg-mgr-model.h b/formal/promela/models/messages/tr-msg-mgr-model.h
new file mode 100644
index 00000000..9af14bd8
--- /dev/null
+++ b/formal/promela/models/messages/tr-msg-mgr-model.h
@@ -0,0 +1,132 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+#ifndef _TR_MODEL_EVENTS_MGR_H
+#define _TR_MODEL_EVENTS_MGR_H
+
+#include <rtems.h>
+#include <rtems/score/thread.h>
+
+#include <rtems/test.h>
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+
+/*
+ * Run Setup/Cleanup structs/functions
+ */
+typedef struct {
+  int this_test_number; // test number used to identify a test runner instance
+  rtems_id receiver_id; // receiver ID used for the event send action.
+  rtems_status_code send_status; // status of the message send action.
+  rtems_option receive_option_set; // option set used for the message receive action
+  rtems_interval receive_timeout; // timeout used for the message receive action
+  rtems_status_code receive_status; // status of the message receive action
+  rtems_status_code create; //status of the messsge queue create action
+  rtems_attribute msg_queue_attr;
+
+  rtems_id queue_id;
+  uint8_t send_msg_counter; 
+  size_t receive_size; //size of messages recieved by receive
+
+  Thread_Control *runner_thread; // TCB of the runner task
+  rtems_id runner_id; // ID of the runner task
+  rtems_id worker1_id; // task ID of the worker task
+  rtems_id worker2_id;
+  rtems_id worker1_wakeup; // ID of the semaphore used to wake up the worker task
+  rtems_id worker2_wakeup;
+  rtems_id runner_wakeup; // ID of the semaphore used to wake up the runner task
+  rtems_id runner_sched; // scheduler ID of scheduler used by the runner task
+  rtems_id other_sched; // scheduler ID of another scheduler
+                        // which is not used by the runner task
+  T_thread_switch_log_4 thread_switch_log; // thread switch log
+} RtemsModelMessageMgr_Context;
+
+typedef enum {
+  PRIO_HIGH = 1,
+  PRIO_NORMAL,
+  PRIO_LOW,
+  PRIO_OTHER
+} Priorities;
+
+#define POWER_OF_10 100
+
+#define WORKER_ATTRIBUTES RTEMS_DEFAULT_ATTRIBUTES
+
+#define MAX_TLS_SIZE RTEMS_ALIGN_UP( 64, RTEMS_TASK_STORAGE_ALIGNMENT )
+
+typedef RtemsModelMessageMgr_Context Context;
+
+rtems_id CreateWakeupSema( void );
+
+void DeleteWakeupSema( rtems_id id );
+
+void Wait( rtems_id id );
+
+void Wakeup( rtems_id id ) ;
+
+rtems_event_set GetPending( Context *ctx );
+
+rtems_option mergeopts( bool wait );
+
+rtems_interval getTimeout( int timeout ) ;
+
+rtems_id idNull( Context *ctx, bool passedid ) ;
+
+rtems_id mapid( Context *ctx, int pid ) ;
+
+void checkTaskIs( rtems_id expected_id ) ;
+
+void ShowWorkerSemaId( Context *ctx ) ;
+
+void ShowRunnerSemaId( Context *ctx ) ;
+
+void initialise_semaphore( Context *ctx, rtems_id semaphore[] );
+
+void RtemsModelMessageMgr_Setup_Wrap( void *arg ) ;
+
+
+void RtemsModelMessageMgr_Teardown_Wrap( void *arg ) ;
+
+size_t RtemsModelMessageMgr_Scope( void *arg, char *buf, size_t n ) ;
+
+void RtemsModelMessageMgr_Cleanup( RtemsModelMessageMgr_Context *ctx );
+
+
+/**
+ * @addtogroup RTEMSTestCaseRtemsModelMessageMgr_Run
+ *
+ * @{
+ */
+
+/**
+ * @brief Runs the parameterized test case.
+ *
+ */
+
+void RtemsModelMessageMgr_Run0(void);
+
+void RtemsModelMessageMgr_Run1(void);
+
+void RtemsModelMessageMgr_Run2(void);
+
+void RtemsModelMessageMgr_Run3(void);
+
+void RtemsModelMessageMgr_Run4(void);
+
+void RtemsModelMessageMgr_Run5(void);
+
+void RtemsModelMessageMgr_Run6(void);
+
+void RtemsModelMessageMgr_Run7(void);
+
+void RtemsModelMessageMgr_Run8(void);
+
+/** @} */
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif /* _TR_EVENT_SEND_RECEIVE_H */