[PATCH 06/18] adds event manager model

Andrew.Butterfield at scss.tcd.ie Andrew.Butterfield at scss.tcd.ie
Thu Dec 22 11:38:42 UTC 2022



---
 formal/promela/models/events/.gitignore       |   1 +
 formal/promela/models/events/STATUS.md        |  21 +
 .../models/events/event-mgr-model-post.h      |   8 +
 .../models/events/event-mgr-model-pre.h       |  51 ++
 .../models/events/event-mgr-model-rfn.yml     | 182 ++++
 .../models/events/event-mgr-model-run.h       | 164 ++++
 .../promela/models/events/event-mgr-model.pml | 848 ++++++++++++++++++
 .../models/events/tc-event-mgr-model.c        | 358 ++++++++
 .../models/events/tr-event-mgr-model.c        | 257 ++++++
 .../models/events/tr-event-mgr-model.h        | 245 +++++
 10 files changed, 2135 insertions(+)
 create mode 100644 formal/promela/models/events/.gitignore
 create mode 100644 formal/promela/models/events/STATUS.md
 create mode 100644 formal/promela/models/events/event-mgr-model-post.h
 create mode 100644 formal/promela/models/events/event-mgr-model-pre.h
 create mode 100644 formal/promela/models/events/event-mgr-model-rfn.yml
 create mode 100644 formal/promela/models/events/event-mgr-model-run.h
 create mode 100644 formal/promela/models/events/event-mgr-model.pml
 create mode 100644 formal/promela/models/events/tc-event-mgr-model.c
 create mode 100644 formal/promela/models/events/tr-event-mgr-model.c
 create mode 100644 formal/promela/models/events/tr-event-mgr-model.h

diff --git a/formal/promela/models/events/.gitignore b/formal/promela/models/events/.gitignore
new file mode 100644
index 00000000..a1fcab96
--- /dev/null
+++ b/formal/promela/models/events/.gitignore
@@ -0,0 +1 @@
+tr-model-events-mgr-*.c
diff --git a/formal/promela/models/events/STATUS.md b/formal/promela/models/events/STATUS.md
new file mode 100644
index 00000000..71518926
--- /dev/null
+++ b/formal/promela/models/events/STATUS.md
@@ -0,0 +1,21 @@
+# EVENT MANAGER status
+
+## 7th Nov 2022 COMPLETE
+
+* Platform: Dell G5, Ubuntu 20.04.5 LTS
+* Generated: OK
+* Compiles: OK
+* Runs: OK
+* All Tests Pass: OK
+
+See `events/archive/20221107-165035`
+
+## 3rd Nov 2022 COMPLETE
+
+* Platform: Dell G5, Ubuntu 20.04.5 LTS
+* Generated: OK
+* Compiles: OK
+* Runs: OK
+* All Tests Pass: OK
+
+See `events/archive/20221103-165851`
diff --git a/formal/promela/models/events/event-mgr-model-post.h b/formal/promela/models/events/event-mgr-model-post.h
new file mode 100644
index 00000000..df2738a4
--- /dev/null
+++ b/formal/promela/models/events/event-mgr-model-post.h
@@ -0,0 +1,8 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+static void Runner( RtemsModelEventsMgr_Context *ctx )
+{
+  T_log( T_NORMAL, "Runner running" );
+  TestSegment4( ctx );
+  T_log( T_NORMAL, "Runner finished" );
+}
diff --git a/formal/promela/models/events/event-mgr-model-pre.h b/formal/promela/models/events/event-mgr-model-pre.h
new file mode 100644
index 00000000..9a764a82
--- /dev/null
+++ b/formal/promela/models/events/event-mgr-model-pre.h
@@ -0,0 +1,51 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * @file
+ *
+ * @ingroup RTEMSTestCaseRtemsModelEventsMgr
+ */
+
+/*
+ * 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-event-mgr-model.h"
diff --git a/formal/promela/models/events/event-mgr-model-rfn.yml b/formal/promela/models/events/event-mgr-model-rfn.yml
new file mode 100644
index 00000000..96727b88
--- /dev/null
+++ b/formal/promela/models/events/event-mgr-model-rfn.yml
@@ -0,0 +1,182 @@
+# SPDX-License-Identifier: BSD-2-Clause
+# Event Manager: Promela to RTEMS Refinement
+
+# Copyright (C) 2019-2021 Trinity College Dublin (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.
+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-events-mgr.c) */
+
+pending_DCL: rtems_event_set {0}[TASK_MAX];
+
+semaphore_DCL: rtems_id {0}[SEMA_MAX];
+
+sendrc_DCL: rtems_status_code
+
+recrc_DCL: rtems_status_code
+
+recout_DCL: rtems_event_set {0}[TASK_MAX];
+
+INIT: |
+  initialise_pending( pending, TASK_MAX );
+  initialise_semaphore( ctx, semaphore );
+
+Runner: |
+  checkTaskIs( ctx->runner_id );
+
+Worker: |
+  checkTaskIs( ctx->worker_id );
+
+SIGNAL: |
+  Wakeup( semaphore[{}] );
+
+WAIT: |
+  Wait( semaphore[{}] );
+
+event_send: |
+  T_log( T_NORMAL, "Calling Send(%d,%d)", mapid( ctx, {1}), {2} );
+  {3} = ( *ctx->send )( mapid( ctx, {1} ), {2} );
+  T_log( T_NORMAL, "Returned 0x%x from Send", {3} );
+
+event_receive: |
+  T_log( T_NORMAL, "Calling Receive(%d,%d,%d,%d)", {0}, mergeopts( {1}, {2} ) ,{3} , {4} ? &recout[{4}] : NULL );
+  {5} = ( *ctx->receive )( {0}, mergeopts( {1}, {2} ), {3}, {4} ? &recout[{4}] : NULL );
+  T_log( T_NORMAL, "Returned 0x%x from Receive", {5} );
+
+sendrc:
+  T_rsc( sendrc, {0} );
+
+recrc:
+  T_rsc( recrc, {0} );
+
+pending: |
+  pending[{0}] = GetPending( ctx );
+  T_eq_int( pending[{0}], {1} );
+
+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_ge_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/events/event-mgr-model-run.h b/formal/promela/models/events/event-mgr-model-run.h
new file mode 100644
index 00000000..324a05d9
--- /dev/null
+++ b/formal/promela/models/events/event-mgr-model-run.h
@@ -0,0 +1,164 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+static void Worker{0}( rtems_task_argument arg )
+{{
+  Context *ctx;
+  rtems_event_set events;
+
+  ctx = (Context *) arg;
+
+  T_log( T_NORMAL, "Worker Running" );
+  TestSegment3( ctx );
+  T_log( T_NORMAL, "Worker finished" );
+
+  // (void) rtems_task_suspend( RTEMS_SELF );
+  // Ensure we hold no semaphores
+  Wakeup( ctx->worker_wakeup );
+  Wakeup( ctx->runner_wakeup );
+  // Wait for events so we don't terminate
+  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 + TEST_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 RtemsModelEventsMgr_Setup{0}(
+  RtemsModelEventsMgr_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;
+
+  T_log( T_NORMAL, "Creating Worker Wakeup Semaphore" );
+  ctx->worker_wakeup = CreateWakeupSema();
+  T_log( T_NORMAL, "Creating Runner Wakeup Semaphore" );
+  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 );
+}}
+
+
+static void RtemsModelEventsMgr_Setup_Wrap{0}( void *arg )
+{{
+  RtemsModelEventsMgr_Context *ctx;
+
+  ctx = arg;
+  RtemsModelEventsMgr_Setup{0}( ctx );
+}}
+
+
+static RtemsModelEventsMgr_Context RtemsModelEventsMgr_Instance{0};
+
+static T_fixture RtemsModelEventsMgr_Fixture{0} = {{
+  .setup = RtemsModelEventsMgr_Setup_Wrap{0},
+  .stop = NULL,
+  .teardown = RtemsModelEventsMgr_Teardown_Wrap,
+  .scope = RtemsModelEventsMgr_Scope,
+  .initial_context = &RtemsModelEventsMgr_Instance{0}
+}};
+
+static T_fixture_node RtemsModelEventsMgr_Node{0};
+
+void RtemsModelEventsMgr_Run{0}(
+  rtems_status_code ( *send )( rtems_id, rtems_event_set ),
+  rtems_status_code ( *receive )( rtems_event_set, rtems_option, rtems_interval, rtems_event_set * ),
+  rtems_event_set (   *get_pending_events )( Thread_Control * ),
+  unsigned int         wait_class,
+  int                  waiting_for_event
+)
+{{
+  RtemsModelEventsMgr_Context *ctx;
+
+  T_set_verbosity( T_NORMAL );
+
+  T_log( T_NORMAL, "Runner Invoked" );
+  T_log( T_NORMAL, "Runner Wait Class: %d", wait_class );
+  T_log( T_NORMAL, "Runner WaitForEvent: %d", waiting_for_event );
+
+  T_log( T_NORMAL, "Pushing Test Fixture..." );
+
+
+  ctx = T_push_fixture(
+    &RtemsModelEventsMgr_Node{0},
+    &RtemsModelEventsMgr_Fixture{0}
+  );
+  // This runs RtemsModelEventsMgr_Fixture
+
+  T_log( T_NORMAL, "Test Fixture Pushed" );
+
+
+  ctx->send = send;
+  ctx->receive = receive;
+  ctx->get_pending_events = get_pending_events;
+  ctx->wait_class = wait_class;
+  ctx->waiting_for_event = waiting_for_event;
+
+  ctx->this_test_number = {0};
+
+  // RtemsModelEventsMgr_Prepare( ctx );
+  ctx->events_to_send = 0;
+  ctx->send_status = RTEMS_INCORRECT_STATE;
+  ctx->received_events = 0xffffffff;
+  ctx->receive_option_set = 0;
+  ctx->receive_timeout = RTEMS_NO_TIMEOUT;
+  ctx->unsatisfied_pending = 0xffffffff;
+  memset( &ctx->thread_switch_log, 0, sizeof( ctx->thread_switch_log ) );
+  T_eq_u32( GetPending( ctx ), 0 );
+  _Thread_Wait_flags_set( ctx->runner_thread, THREAD_WAIT_CLASS_PERIOD );
+
+  TestSegment0( ctx );
+
+  Runner( ctx );
+
+  RtemsModelEventsMgr_Cleanup( ctx );
+
+  T_log( T_NORMAL, "Run Pop Fixture" );
+  ShowWorkerSemaId( ctx );
+  T_pop_fixture();
+  ShowWorkerSemaId( ctx );
+}}
+
+/** @}} */
diff --git a/formal/promela/models/events/event-mgr-model.pml b/formal/promela/models/events/event-mgr-model.pml
new file mode 100644
index 00000000..9bfa255b
--- /dev/null
+++ b/formal/promela/models/events/event-mgr-model.pml
@@ -0,0 +1,848 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/*
+ * event-mgr-model.pml
+ *
+ * Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+ *
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ *     * Redistributions of source code must retain the above copyright
+ *       notice, this list of conditions and the following disclaimer.
+ *
+ *     * 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.
+ *
+ *     * Neither the name of the copyright holders nor the names of its
+ *       contributors may be used to endorse or promote products derived
+ *       from this software without specific prior written permission.
+ *
+ * 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.
+ */
+
+/*
+ * The model presented here is designed to work with the following files:
+ *   Refinement:   model-events-mgr-rfn.yml
+ *   Test Preamble: model-events-mgr-pre.h
+ *   Test Postamble: model-events-mgr-post.h
+ *   Test Runner: model-events-mgr-run.h
+ */
+
+/*
+ * We need to output annotations for any #define we use.
+ * It is simplest to keep them all together,
+ * and use an inline to output them.
+ */
+
+// Event Sets - we only support 4 events, rather than 32
+#define NO_OF_EVENTS 4
+#define EVTS_NONE 0
+#define EVTS_PENDING 0
+#define EVT_0 1
+#define EVT_1 2
+#define EVT_2 4
+#define EVT_3 8
+#define EVTS_ALL 15
+#define NO_TIMEOUT 0
+
+// We envisage two RTEMS tasks involved, at most.
+#define TASK_MAX 3 // These are the "RTEMS" tasks only, numbered 1 & 2
+                   // We reserve 0 to model NULL pointers
+
+// We use two semaphores to synchronise the tasks
+#define SEMA_MAX 2
+
+// IDs here index an array, so we use the largest bad index as a bad id
+#define BAD_ID TASK_MAX
+
+// Return Values - ultimately, we should #include these
+// Defined in cpukit/include/rtems/rtems/status.h
+#define RC_OK      0  // RTEMS_SUCCESSFUL
+#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
+
+
+inline outputDefines () {
+   printf("@@@ %d DEF NO_OF_EVENTS %d\n",_pid,NO_OF_EVENTS);
+   printf("@@@ %d DEF EVTS_NONE %d\n",_pid,EVTS_NONE);
+   printf("@@@ %d DEF EVTS_PENDING %d\n",_pid,EVTS_PENDING);
+   printf("@@@ %d DEF EVT_0 %d\n",_pid,EVT_0);
+   printf("@@@ %d DEF EVT_1 %d\n",_pid,EVT_1);
+   printf("@@@ %d DEF EVT_2 %d\n",_pid,EVT_2);
+   printf("@@@ %d DEF EVT_3 %d\n",_pid,EVT_3);
+   printf("@@@ %d DEF EVTS_ALL %d\n",_pid,EVTS_ALL);
+   printf("@@@ %d DEF NO_TIMEOUT %d\n",_pid,NO_TIMEOUT);
+   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 RC_OK RTEMS_SUCCESSFUL\n",_pid);
+   printf("@@@ %d DEF RC_InvId RTEMS_INVALID_ID\n",_pid);
+   printf("@@@ %d DEF RC_InvAddr RTEMS_INVALID_ADDRESS\n",_pid);
+   printf("@@@ %d DEF RC_Unsat RTEMS_UNSATISFIED\n",_pid);
+   printf("@@@ %d DEF RC_Timeout RTEMS_TIMEOUT\n",_pid);
+}
+
+
+
+// Special values: task states, options, return codes
+mtype = {
+  Zombie, Ready, EventWait, TimeWait, OtherWait, // Task states
+  Wait, NoWait, All, Any, // 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
+  unsigned wanted  : NO_OF_EVENTS ; // EvtSet, those expected by receiver
+  unsigned pending : NO_OF_EVENTS ; // EvtSet, those already received
+  bool all; // Do we want All?
+};
+
+
+Task tasks[TASK_MAX]; // tasks[0] models a NULL dereference
+
+byte sendrc;            // Sender global variable
+byte recrc;             // Receiver global variable
+byte recout[TASK_MAX] ; // models receive 'out' location.
+
+/*
+ * Running Orders (maintained by simple global sync counter):
+ *   Receive;;Send  =  Receive;Release(1) || Obtain(1);Send
+ * Here ;; is "sequential" composition of *different* threads
+ */
+bool semaphore[SEMA_MAX]; // Semaphore
+
+inline outputDeclarations () {
+  printf("@@@ %d DECL byte sendrc 0\n",_pid);
+  printf("@@@ %d DECL byte recrc 0\n",_pid);
+  // Rather than refine an entire Task array, we refine array 'slices'
+  printf("@@@ %d DCLARRAY EvtSet pending TASK_MAX\n",_pid);
+  printf("@@@ %d DCLARRAY byte recout TASK_MAX\n",_pid);
+  printf("@@@ %d DCLARRAY Semaphore semaphore SEMA_MAX\n",_pid);
+}
+
+/*
+ * 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 ;
+}
+
+
+inline printevents (evts) {
+  printf("{%d,%d,%d,%d}",(evts)/8%2,(evts)/4%2,(evts)/2%2,(evts)%2);
+}
+
+inline events(evts,e3,e2,e1,e0) {
+  evts = (8*e3+4*e2+2*e1+e0);
+}
+
+inline setminus(diff,minuend,subtrahend) {
+  diff = (minuend) & (15-(subtrahend))
+}
+
+
+/* The following inlines are not given here as atomic,
+ * but are intended to be used in an atomic context.
+*/
+
+inline nl() { printf("\n") } // Useful shorthand
+
+/*
+ * 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)
+}
+
+/*
+ * satisfied(task,out,sat) checks if a recieve has been satisfied.
+ * It updates its `sat` argument to reflect the check outcome,
+ * and logs relevant details.
+ */
+inline satisfied(task,out,sat) {
+  out = task.pending & task.wanted;
+  if
+  ::  task.all && out == task.wanted  ->  sat = true
+  ::  !task.all && out != EVTS_NONE   ->  sat = true
+  ::  else                            ->  sat = false
+  fi
+  printf("@@@ %d LOG satisfied(<pnd:%d wnt:%d all:%d>,out:%d,SAT:%d)\n",
+          _pid,task.pending,task.wanted,task.all,out,sat)
+}
+
+/*
+ * preemptIfRequired(sendid,rcvid) is executed,
+ * when task[rcvid] has had its receive request satisfied
+ * by a send from task[sendid].
+ *
+ * It is invoked by the send operation in this model.
+ *
+ * It checks if task[sendid] should be preempted, and makes it so.
+ * This is achieved here by setting the task state to OtherWait.
+ */
+inline preemptIfRequired(sendid,rcvid) {
+  if
+  ::  tasks[sendid].preemptable  &&
+      // we use the (usual?) convention that higher priority is a lower number
+      tasks[rcvid].prio < tasks[sendid].prio &&
+      tasks[rcvid].state == Ready
+      ->  tasks[sendid].state = OtherWait;
+          printf("@@@ %d STATE %d OtherWait\n",_pid,sendid)
+  ::  else
+  fi
+}
+
+/*
+ * event_send(self,tid,evts,rc)
+ *
+ * Simulates a call to rtems_event_send
+ *   self : id of process modelling the task/IDR making call
+ *   tid  : id of process modelling the target task of the call
+ *   evts : event set being sent
+ *   rc : updated with the return code when the send completes
+ *
+ * Corresponding RTEMS call:
+ *   rc = rtems_event_send(tid,evts);
+ *     `tid`  models `rtems_id id`
+ *     `evts` models `rtems_event_set event_in`
+ *
+ * Modelling the call, as described above, is straightforward.
+ * Modelling the behaviour less so, because of the requirement to preempt,
+ * under certain circumstances.
+ */
+inline event_send(self,tid,evts,rc) {
+  atomic{
+    if
+    ::  tid >= BAD_ID -> rc = RC_InvId
+    ::  tid < BAD_ID ->
+        tasks[tid].pending = tasks[tid].pending | evts
+        // at this point, have we woken the target task?
+        unsigned got : NO_OF_EVENTS;
+        bool sat;
+        satisfied(tasks[tid],got,sat);
+        if
+        ::  sat ->
+            tasks[tid].state = Ready;
+            printf("@@@ %d STATE %d Ready\n",_pid,tid)
+            preemptIfRequired(self,tid) ;
+            // tasks[self].state may now be OtherWait !
+            /* if
+            :: tasks[self].state == OtherWait -> Released(sendSema)
+            :: else
+            fi */
+            waitUntilReady(self);
+        ::  else -> skip
+        fi
+        rc = RC_OK;
+    fi
+  }
+}
+
+/*
+ * event_receive(self,evts,wait,wantall,interval,out,rc)
+ *
+ * Simulates a call to rtems_event_receive
+ *   self : id of process modelling the task making call
+ *   evts : input event set
+ *   wait : true if receive should wait
+ *   what : all, or some?
+ *   interval : wait interval (0 waits forever)
+ *   out : pointer to location
+ *         updated with the satisfying events when the receive completes
+ *   rc : updated with the return code when the receive completes
+ *
+ * Corresponding RTEMS call:
+ *   opts = mergeopts(wait,wantall);
+ *   rc = rtems_event_receive(evts,opts,interval,out);
+ *     `evts` models `rtems_event_set event_in`
+ *     `when` models the waiting aspect of the option set
+ *     `what` models the how much aspect of the option set
+ *     `opt` models `rtems_option option_set`, a fusion of `wait` and `wantall`
+ *       this fusion `(bool,bool)->rtems_option`
+ *       is done by C code `mergeopts`, defined in the preamble.
+ *     `interval` models `rtems_interval ticks`
+ *     `out` models `rtems_event_set *event_out`
+ *
+ *
+ */
+inline event_receive(self,evts,wait,wantall,interval,out,rc){
+  atomic{
+    printf("@@@ %d LOG pending[%d] = ",_pid,self);
+    printevents(tasks[self].pending); nl();
+    tasks[self].wanted = evts;
+    tasks[self].all = wantall
+    if
+    ::  out == 0 ->
+        printf("@@@ %d LOG Receive NULL out.\n",_pid);
+        rc = RC_InvAddr ;
+    ::  evts == EVTS_PENDING ->
+        printf("@@@ %d LOG Receive Pending.\n",_pid);
+        recout[out] = tasks[self].pending;
+        rc = RC_OK
+    ::  else ->
+        bool sat;
+        retry:  satisfied(tasks[self],recout[out],sat);
+        if
+        ::  sat ->
+            printf("@@@ %d LOG Receive Satisfied!\n",_pid);
+            setminus(tasks[self].pending,tasks[self].pending,recout[out]);
+            printf("@@@ %d LOG pending'[%d] = ",_pid,self);
+            printevents(tasks[self].pending); nl();
+            rc = RC_OK;
+        ::  !sat && !wait ->
+            printf("@@@ %d LOG Receive Not Satisfied (no wait)\n",_pid);
+            rc = RC_Unsat;
+        ::  !sat && wait && interval > 0 ->
+            printf("@@@ %d LOG Receive Not Satisfied (timeout %d)\n",_pid,interval);
+            tasks[self].ticks = interval;
+            tasks[self].tout = false;
+            tasks[self].state = TimeWait;
+            printf("@@@ %d STATE %d TimeWait %d\n",_pid,self,interval)
+            waitUntilReady(self);
+            if
+            ::  tasks[self].tout  ->  rc = RC_Timeout
+            ::  else              ->  goto retry
+            fi
+        ::  else -> // !sat && wait && interval <= 0
+            printf("@@@ %d LOG Receive Not Satisfied (wait).\n",_pid);
+            tasks[self].state = EventWait;
+            printf("@@@ %d STATE %d EventWait\n",_pid,self)
+            if
+            :: sendTwice && !sentFirst -> Released(sendSema);
+            :: else
+            fi
+            waitUntilReady(self);
+            goto retry
+        fi
+    fi
+    printf("@@@ %d LOG pending'[%d] = ",_pid,self);
+    printevents(tasks[self].pending); nl();
+  }
+}
+
+
+/*
+ * Model Processes
+ * We shall use four processes in this model.
+ *  Two will represent the RTEMS send and receive tasks
+ *  One will model a timer
+ *  One will model scheduling and other task management behaviour.
+ */
+
+// These are not output to test generation
+#define SEND_ID 1
+#define RCV_ID 2
+#define THIS_NODE 0
+#define THAT_NODE 1
+#define MAX_STEPS 3
+#define MAX_WAIT 10
+
+/*
+ * Scenario Generation
+ */
+
+ /*
+ * Send variants:
+ *   self = SEND_ID
+ *   tid in {BAD_ID,RCV_ID,SEND_ID}
+ *   evts in a "suitable" subset of all events.
+ *   prio in low, medium, high
+ */
+typedef SendInputs {
+  byte target_id ;
+  unsigned send_evts : NO_OF_EVENTS ;
+} ;
+SendInputs  send_in[MAX_STEPS];
+
+ /*
+ * Receive variants:
+ *   self in {RCV_ID,SEND_ID}, latter requires send.tid = SEND_ID
+ *   evts in "suitable" subset of all events.
+ *   wait in {true,false}, a.k.a. {Wait,NoWait}
+ *   wantall in {true,false}, a.k.a. {All,Any}
+ *   interval in {0..MAX_WAIT}
+ *   prio = medium
+ */
+typedef ReceiveInputs {
+  unsigned receive_evts : NO_OF_EVENTS ;
+  bool will_wait;
+  bool everything;
+  byte wait_length;
+};
+ReceiveInputs receive_in[MAX_STEPS];
+
+
+/*
+ * Sender Scenario
+ *   vary: priority, preemptable,target,events
+ */
+bool doSend; // false for receive-only scenarios
+bool sendTwice;
+bool sentFirst;
+byte sendPrio;
+bool sendPreempt;
+byte sendTarget;
+unsigned sendEvents : NO_OF_EVENTS
+unsigned sendEvents1 : NO_OF_EVENTS
+unsigned sendEvents2 : NO_OF_EVENTS
+
+/*
+ * Receiver Scenario
+ *   vary: events,wanted,wait,interval,
+ *   fixed: priority (mid)
+ */
+bool doReceive; // false for send-only scenarios
+unsigned rcvEvents : NO_OF_EVENTS;
+bool rcvWait;
+bool rcvAll;
+int rcvInterval;
+int rcvOut;
+byte rcvPrio;
+
+
+/*
+ * Semaphore Setup
+ */
+int sendSema;
+int rcvSema;
+int startSema;
+
+/*
+ * Multicore setup
+ */
+bool multicore;
+int sendCore;
+int rcvCore;
+
+/*
+ * Generating Scenarios
+ *
+ * We consider the following broad scenario classes:
+ *
+ *   Send only - check for bad target ids
+ *   Receive only - check for timeouts, etc.
+ *   Send ; Receive - check correct event transmission
+ *   Receive ; Send - check waiting, event transmission and preemption
+ *
+ * Issues to do with sending to self, or to another node,
+ * can be covered in Send; Receive.
+ */
+mtype = {Send,Receive,SndRcv,RcvSnd,SndRcvSnd,SndPre, MultiCore};
+mtype scenario;
+
+inline chooseScenario() {
+
+  // Common Defaults
+  doSend = true;
+  doReceive = true;
+  sendTwice = false;
+  sentFirst = false;
+  semaphore[0] = false;
+  semaphore[1] = false;
+  sendPrio = 2;
+  sendPreempt = false;
+  sendTarget = RCV_ID;
+  rcvPrio = 2;
+  rcvWait = true;
+  rcvAll = true;
+  rcvInterval = 0;
+  rcvOut = RCV_ID ;
+  tasks[SEND_ID].state = Ready;
+  tasks[RCV_ID].state = Ready;
+
+  sendEvents1 = 10; // {1,0,1,0}
+  sendEvents2 = 0; // {0,0,0,0}
+  sendEvents = sendEvents1;
+  rcvEvents  = 10; // {1,0,1,0}
+  sendSema = 0;
+  rcvSema = 1;
+  startSema = sendSema;
+
+  multicore = false;
+  sendCore = 0;
+  rcvCore = 0;
+
+  if
+  ::  scenario = Send;
+  ::  scenario = Receive;
+  ::  scenario = SndRcv;
+  ::  scenario = SndPre;
+  ::  scenario = SndRcvSnd;
+  ::  scenario = MultiCore;
+  fi
+  atomic{printf("@@@ %d LOG scenario ",_pid); printm(scenario); nl()} ;
+
+
+  if
+  ::  scenario == Send ->
+        doReceive = false;
+        sendTarget = BAD_ID;
+  ::  scenario == Receive ->
+        doSend = false
+        if
+        :: rcvWait = false
+        :: rcvWait = true; rcvInterval = 4
+        :: rcvOut = 0;
+        fi
+        printf( "@@@ %d LOG sub-senario wait:%d interval:%d, out:%d\n",
+                _pid, rcvWait, rcvInterval, rcvOut )
+  ::  scenario == SndRcv ->
+        if
+        ::  sendEvents = 14; // {1,1,1,0}
+        ::  sendEvents = 11; // {1,0,1,1}
+        ::  rcvEvents = EVTS_PENDING;
+        ::  rcvEvents = EVTS_ALL;
+            rcvWait = false;
+            rcvAll = false;
+        fi
+        printf( "@@@ %d LOG sub-senario send/receive events:%d/%d\n",
+                _pid, sendEvents, rcvEvents )
+  ::  scenario == SndPre ->
+        sendPrio = 3;
+        sendPreempt = true;
+        startSema = rcvSema;
+        printf( "@@@ %d LOG sub-senario send-preemptable events:%d\n",
+                _pid, sendEvents )
+  ::  scenario == SndRcvSnd ->
+        sendEvents1 = 2; // {0,0,1,0}
+        sendEvents2 = 8; // {1,0,0,0}
+        sendEvents = sendEvents1;
+        sendTwice = true;
+        printf( "@@@ %d LOG sub-senario send-receive-send events:%d\n",
+                _pid, sendEvents )
+  ::  scenario == MultiCore ->
+        multicore = true;
+        sendCore = 1;
+        printf( "@@@ %d LOG sub-senario multicore send-receive events:%d\n",
+                _pid, sendEvents )
+  ::  else // go with defaults
+  fi
+
+}
+
+
+proctype Sender (byte nid, taskid) {
+
+  tasks[taskid].nodeid = nid;
+  tasks[taskid].pmlid = _pid;
+  tasks[taskid].prio = sendPrio;
+  tasks[taskid].preemptable = sendPreempt;
+  tasks[taskid].state = Ready;
+  printf("@@@ %d TASK Worker\n",_pid);
+  /* printf("@@@ %d LOG Sender Task %d running on Node %d\n",_pid,taskid,nid); */
+
+  if
+  :: multicore ->
+       // printf("@@@ %d CALL OtherScheduler %d\n", _pid, sendCore);
+       printf("@@@ %d CALL SetProcessor %d\n", _pid, sendCore);
+  :: else
+  fi
+
+  if
+  :: sendPrio > rcvPrio -> printf("@@@ %d CALL LowerPriority\n", _pid);
+  :: sendPrio == rcvPrio -> printf("@@@ %d CALL EqualPriority\n", _pid);
+  :: sendPrio < rcvPrio -> printf("@@@ %d CALL HigherPriority\n", _pid);
+  :: else
+  fi
+
+repeat:
+
+  Obtain(sendSema);
+
+  if
+  :: doSend ->
+    if
+    :: !sentFirst -> printf("@@@ %d CALL StartLog\n",_pid);
+    :: else
+    fi
+    printf("@@@ %d CALL event_send %d %d %d sendrc\n",_pid,taskid,sendTarget,sendEvents);
+
+    if
+    :: sendPreempt && !sentFirst -> printf("@@@ %d CALL CheckPreemption\n",_pid);
+    :: !sendPreempt && !sentFirst -> printf("@@@ %d CALL CheckNoPreemption\n",_pid);
+    :: else
+    fi
+
+           /* (self,  tid,       evts,      rc) */
+    event_send(taskid,sendTarget,sendEvents,sendrc);
+
+    printf("@@@ %d SCALAR sendrc %d\n",_pid,sendrc);
+  :: else
+  fi
+
+  Release(rcvSema);
+
+  if
+  :: sendTwice && !sentFirst ->
+     sentFirst = true;
+     sendEvents = sendEvents2;
+     goto repeat;
+  :: else
+  fi
+
+  printf("@@@ %d LOG Sender %d finished\n",_pid,taskid);
+  tasks[taskid].state = Zombie;
+  printf("@@@ %d STATE %d Zombie\n",_pid,taskid)
+}
+
+
+proctype Receiver (byte nid, taskid) {
+
+  tasks[taskid].nodeid = nid;
+  tasks[taskid].pmlid = _pid;
+  tasks[taskid].prio = rcvPrio;
+  tasks[taskid].preemptable = false;
+  tasks[taskid].state = Ready;
+  printf("@@@ %d TASK Runner\n",_pid,taskid);
+
+  if
+  :: multicore ->
+       // printf("@@@ %d CALL RunnerScheduler %d\n", _pid, rcvCore);
+       printf("@@@ %d CALL SetProcessor %d\n", _pid, rcvCore);
+  :: else
+  fi
+
+  Release(startSema); // make sure stuff starts */
+  /* printf("@@@ %d LOG Receiver Task %d running on Node %d\n",_pid,taskid,nid); */
+
+  Obtain(rcvSema);
+
+  // If the receiver is higher priority then it will be running
+  // The sender is either blocked waiting for its semaphore
+  // or because it is lower priority.
+  // A high priority receiver needs to release the sender now, before it
+  // gets blocked on its own event receive.
+  if
+  :: rcvPrio < sendPrio -> Release(sendSema);  // Release send semaphore for preemption
+  :: else
+  fi
+
+  if
+  :: doReceive ->
+    printf("@@@ %d SCALAR pending %d %d\n",_pid,taskid,tasks[taskid].pending);
+
+    if
+    :: sendTwice && !sentFirst -> Release(sendSema)
+    :: else
+    fi
+
+    printf("@@@ %d CALL event_receive %d %d %d %d %d recrc\n",
+           _pid,rcvEvents,rcvWait,rcvAll,rcvInterval,rcvOut);
+
+              /* (self,  evts,     when,   what,  ticks,      out,   rc) */
+    event_receive(taskid,rcvEvents,rcvWait,rcvAll,rcvInterval,rcvOut,recrc);
+
+    printf("@@@ %d SCALAR recrc %d\n",_pid,recrc);
+    if
+    :: rcvOut > 0 ->
+      printf("@@@ %d SCALAR recout %d %d\n",_pid,rcvOut,recout[rcvOut]);
+    :: else
+    fi
+    printf("@@@ %d SCALAR pending %d %d\n",_pid,taskid,tasks[taskid].pending);
+  :: else
+  fi
+
+  /*  Again, not sure this is a good idea
+  if
+  :: rcvPrio >= sendPrio -> Release(sendSema);
+  :: rcvPrio < sendPrio -> Obtain(rcvSema);  // Allow send task to complete after preemption
+  :: else
+  fi
+  */
+  Release(sendSema);
+
+  printf("@@@ %d LOG Receiver %d finished\n",_pid,taskid);
+  tasks[taskid].state = Zombie;
+  printf("@@@ %d STATE %d Zombie\n",_pid,taskid)
+}
+
+bool stopclock = false;
+
+/*
+ * 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.
+ */
+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("Event Manager Model running.\n");
+  printf("Setup...\n");
+
+  printf("@@@ %d NAME Event_Manager_TestGen\n",_pid)
+  outputDefines();
+  outputDeclarations();
+
+  printf("@@@ %d INIT\n",_pid);
+  chooseScenario();
+
+
+
+  printf("Run...\n");
+
+  run System();
+  run Clock();
+
+  run Sender(THIS_NODE,SEND_ID);
+  run Receiver(THIS_NODE,RCV_ID);
+
+  _nr_pr == 1;
+
+#ifdef TEST_GEN
+  assert(false);
+#endif
+
+  printf("Event Manager Model finished !\n")
+}
diff --git a/formal/promela/models/events/tc-event-mgr-model.c b/formal/promela/models/events/tc-event-mgr-model.c
new file mode 100644
index 00000000..3c16b360
--- /dev/null
+++ b/formal/promela/models/events/tc-event-mgr-model.c
@@ -0,0 +1,358 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * @file
+ *
+ * @ingroup RTEMSTestCaseRtemsEventValSendReceive
+ * @ingroup RTEMSTestCaseRtemsEventValSystemSendReceive
+ */
+
+/*
+ * 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-event-mgr-model.h"
+
+#include <rtems/test.h>
+
+/**
+ * @defgroup RTEMSTestCaseRtemsEventValSendReceive \
+ *   spec:/rtems/event/val/send-receive
+ *
+ * @ingroup RTEMSTestSuiteTestsuitesValidation0
+ *
+ * @brief Tests the rtems_event_send and rtems_event_receive directives.
+ *
+ * This test case performs the following actions:
+ *
+ * - Run the event send and receive tests for the application event set defined
+ *   by /rtems/event/req/send-receive.
+ *
+ * @{
+ */
+
+static rtems_status_code EventSend(
+  rtems_id        id,
+  rtems_event_set event_in
+)
+{
+  return rtems_event_send( id, event_in );
+}
+
+static rtems_status_code EventReceive(
+  rtems_id         event_in,
+  rtems_option     option_set,
+  rtems_interval   ticks,
+  rtems_event_set *event_out
+)
+{
+  return rtems_event_receive( event_in, option_set, ticks, event_out );
+}
+
+static rtems_event_set GetPendingEvents( Thread_Control *thread )
+{
+  RTEMS_API_Control *api;
+
+  api = thread->API_Extensions[ THREAD_API_RTEMS ];
+  return api->Event.pending_events;
+}
+
+/**
+ * @fn void T_case_body_RtemsEventValSendReceive( void )
+ */
+T_TEST_CASE( RtemsModelEventsMgr0 )
+{
+  RtemsModelEventsMgr_Run0(
+    EventSend,
+    EventReceive,
+    GetPendingEvents,
+    THREAD_WAIT_CLASS_EVENT,
+    STATES_WAITING_FOR_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelEventsMgr1 )
+{
+  RtemsModelEventsMgr_Run1(
+    EventSend,
+    EventReceive,
+    GetPendingEvents,
+    THREAD_WAIT_CLASS_EVENT,
+    STATES_WAITING_FOR_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelEventsMgr2 )
+{
+  RtemsModelEventsMgr_Run2(
+    EventSend,
+    EventReceive,
+    GetPendingEvents,
+    THREAD_WAIT_CLASS_EVENT,
+    STATES_WAITING_FOR_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelEventsMgr3 )
+{
+  RtemsModelEventsMgr_Run3(
+    EventSend,
+    EventReceive,
+    GetPendingEvents,
+    THREAD_WAIT_CLASS_EVENT,
+    STATES_WAITING_FOR_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelEventsMgr4 )
+{
+  RtemsModelEventsMgr_Run4(
+    EventSend,
+    EventReceive,
+    GetPendingEvents,
+    THREAD_WAIT_CLASS_EVENT,
+    STATES_WAITING_FOR_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelEventsMgr5 )
+{
+  RtemsModelEventsMgr_Run5(
+    EventSend,
+    EventReceive,
+    GetPendingEvents,
+    THREAD_WAIT_CLASS_EVENT,
+    STATES_WAITING_FOR_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelEventsMgr6 )
+{
+  RtemsModelEventsMgr_Run6(
+    EventSend,
+    EventReceive,
+    GetPendingEvents,
+    THREAD_WAIT_CLASS_EVENT,
+    STATES_WAITING_FOR_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelEventsMgr7 )
+{
+  RtemsModelEventsMgr_Run7(
+    EventSend,
+    EventReceive,
+    GetPendingEvents,
+    THREAD_WAIT_CLASS_EVENT,
+    STATES_WAITING_FOR_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelEventsMgr8 )
+{
+  RtemsModelEventsMgr_Run8(
+    EventSend,
+    EventReceive,
+    GetPendingEvents,
+    THREAD_WAIT_CLASS_EVENT,
+    STATES_WAITING_FOR_EVENT
+  );
+}
+
+/** @} */
+
+/**
+ * @defgroup RTEMSTestCaseRtemsEventValSystemSendReceive \
+ *   spec:/rtems/event/val/system-send-receive
+ *
+ * @ingroup RTEMSTestSuiteTestsuitesValidation0
+ *
+ * @brief Tests the rtems_event_system_send and rtems_event_system_receive
+ *   directives.
+ *
+ * This test case performs the following actions:
+ *
+ * - Run the event send and receive tests for the system event set defined by
+ *   /rtems/event/req/send-receive.
+ *
+ * @{
+ */
+
+static rtems_status_code EventSystemSend(
+  rtems_id        id,
+  rtems_event_set event_in
+)
+{
+  return rtems_event_system_send( id, event_in );
+}
+
+static rtems_status_code EventSystemReceive(
+  rtems_id         event_in,
+  rtems_option     option_set,
+  rtems_interval   ticks,
+  rtems_event_set *event_out
+)
+{
+  return rtems_event_system_receive(
+    event_in,
+    option_set,
+    ticks,
+    event_out
+  );
+}
+
+static rtems_event_set GetPendingSystemEvents( Thread_Control *thread )
+{
+  RTEMS_API_Control *api;
+
+  api = thread->API_Extensions[ THREAD_API_RTEMS ];
+  return api->System_event.pending_events;
+}
+
+/**
+ * @fn void T_case_body_RtemsEventValSystemSendReceive( void )
+ */
+T_TEST_CASE( RtemsModelSystemEventsMgr0 )
+{
+  RtemsModelEventsMgr_Run0(
+    EventSystemSend,
+    EventSystemReceive,
+    GetPendingSystemEvents,
+    THREAD_WAIT_CLASS_SYSTEM_EVENT,
+    STATES_WAITING_FOR_SYSTEM_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelSystemEventsMgr1 )
+{
+  RtemsModelEventsMgr_Run1(
+    EventSystemSend,
+    EventSystemReceive,
+    GetPendingSystemEvents,
+    THREAD_WAIT_CLASS_SYSTEM_EVENT,
+    STATES_WAITING_FOR_SYSTEM_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelSystemEventsMgr2 )
+{
+  RtemsModelEventsMgr_Run2(
+    EventSystemSend,
+    EventSystemReceive,
+    GetPendingSystemEvents,
+    THREAD_WAIT_CLASS_SYSTEM_EVENT,
+    STATES_WAITING_FOR_SYSTEM_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelSystemEventsMgr3 )
+{
+  RtemsModelEventsMgr_Run3(
+    EventSystemSend,
+    EventSystemReceive,
+    GetPendingSystemEvents,
+    THREAD_WAIT_CLASS_SYSTEM_EVENT,
+    STATES_WAITING_FOR_SYSTEM_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelSystemEventsMgr4 )
+{
+  RtemsModelEventsMgr_Run4(
+    EventSystemSend,
+    EventSystemReceive,
+    GetPendingSystemEvents,
+    THREAD_WAIT_CLASS_SYSTEM_EVENT,
+    STATES_WAITING_FOR_SYSTEM_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelSystemEventsMgr5 )
+{
+  RtemsModelEventsMgr_Run5(
+    EventSystemSend,
+    EventSystemReceive,
+    GetPendingSystemEvents,
+    THREAD_WAIT_CLASS_SYSTEM_EVENT,
+    STATES_WAITING_FOR_SYSTEM_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelSystemEventsMgr6 )
+{
+  RtemsModelEventsMgr_Run6(
+    EventSystemSend,
+    EventSystemReceive,
+    GetPendingSystemEvents,
+    THREAD_WAIT_CLASS_SYSTEM_EVENT,
+    STATES_WAITING_FOR_SYSTEM_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelSystemEventsMgr7 )
+{
+  RtemsModelEventsMgr_Run7(
+    EventSystemSend,
+    EventSystemReceive,
+    GetPendingSystemEvents,
+    THREAD_WAIT_CLASS_SYSTEM_EVENT,
+    STATES_WAITING_FOR_SYSTEM_EVENT
+  );
+}
+
+T_TEST_CASE( RtemsModelSystemEventsMgr8 )
+{
+  RtemsModelEventsMgr_Run8(
+    EventSystemSend,
+    EventSystemReceive,
+    GetPendingSystemEvents,
+    THREAD_WAIT_CLASS_SYSTEM_EVENT,
+    STATES_WAITING_FOR_SYSTEM_EVENT
+  );
+}
+
+/** @} */
diff --git a/formal/promela/models/events/tr-event-mgr-model.c b/formal/promela/models/events/tr-event-mgr-model.c
new file mode 100644
index 00000000..59d0ef4d
--- /dev/null
+++ b/formal/promela/models/events/tr-event-mgr-model.c
@@ -0,0 +1,257 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * @file
+ *
+ * @ingroup RTEMSTestCaseRtemsModelEventsMgr
+ */
+
+/*
+ * 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-event-mgr-model.h"
+
+static const char PromelaModelEventsMgr[] = "/PML-EventsMgr";
+
+#define INPUT_EVENTS ( RTEMS_EVENT_5 | RTEMS_EVENT_23 )
+
+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_event_set GetPending( Context *ctx )
+{
+  rtems_event_set pending;
+  rtems_status_code sc;
+
+  sc = ( *ctx->receive )(
+    RTEMS_PENDING_EVENTS,
+    RTEMS_DEFAULT_OPTIONS,
+    0,
+    &pending
+  );
+  T_quiet_rsc_success( sc );
+
+  return pending;
+}
+
+
+rtems_option mergeopts( bool wait, bool wantall )
+{
+  rtems_option opts;
+
+  if ( wait ) { opts = RTEMS_WAIT; }
+  else { opts = RTEMS_NO_WAIT; } ;
+  if ( wantall ) { opts |= RTEMS_EVENT_ALL; }
+  else { opts |= RTEMS_EVENT_ANY; } ;
+  return opts;
+}
+
+
+/*
+ * Here we need a mapping from model "task numbers/names" to thread Id's here
+ *  Promela Process 3 corresponds to Task 0 (Worker), doing Send
+ *  Promela Process 4 corresponds to Task 1 (Runner), doing Receive
+ */
+rtems_id mapid( Context *ctx, int pid )
+{
+  rtems_id mapped_id;
+
+  switch ( pid ) {
+    case 1 : mapped_id = ctx->worker_id ; break;
+    case 2 : mapped_id = ctx->runner_id; break;
+    default : mapped_id = 0xffffffff; break;
+  }
+  return mapped_id;
+}
+
+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->worker_wakeup;
+  semaphore[1] = ctx->runner_wakeup;
+}
+
+void ShowWorkerSemaId( Context *ctx ) {
+  T_printf( "L:ctx->worker_wakeup = %d\n", ctx->worker_wakeup );
+}
+
+void ShowRunnerSemaId( Context *ctx ) {
+  T_printf( "L:ctx->runner_wakeup = %d\n", ctx->runner_wakeup );
+}
+
+static void RtemsModelEventsMgr_Teardown(
+  RtemsModelEventsMgr_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->worker_id != 0 ) {
+    T_printf( "L:Deleting Task id : %d\n", ctx->worker_id );
+    sc = rtems_task_delete( ctx->worker_id );
+    T_rsc_success( sc );
+  }
+
+  T_log( T_NORMAL, "Deleting Worker Wakeup Semaphore" );
+  DeleteWakeupSema( ctx->worker_wakeup );
+  T_log( T_NORMAL, "Deleting Runner Wakeup Semaphore" );
+  DeleteWakeupSema( ctx->runner_wakeup );
+}
+
+void RtemsModelEventsMgr_Teardown_Wrap( void *arg )
+{
+  RtemsModelEventsMgr_Context *ctx;
+
+  ctx = arg;
+  RtemsModelEventsMgr_Teardown( ctx );
+}
+
+
+size_t RtemsModelEventsMgr_Scope( void *arg, char *buf, size_t n )
+{
+  RtemsModelEventsMgr_Context *ctx;
+  size_t m;
+  int p10;
+  int tnum ;
+  char digit;
+
+  ctx = arg;
+  p10 = POWER_OF_10;
+
+  m = T_str_copy(buf, PromelaModelEventsMgr, 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 RtemsModelEventsMgr_Cleanup(
+  RtemsModelEventsMgr_Context *ctx
+)
+{
+  rtems_status_code sc;
+  rtems_event_set events;
+
+  events = 0;
+  sc = ( *ctx->receive )(
+    RTEMS_ALL_EVENTS,
+    RTEMS_NO_WAIT | RTEMS_EVENT_ANY,
+    0,
+    &events
+  );
+  if ( sc == RTEMS_SUCCESSFUL ) {
+    T_quiet_ne_u32( events, 0 );
+  } else {
+    T_quiet_rsc( sc, RTEMS_UNSATISFIED );
+    T_quiet_eq_u32( events, 0 );
+  }
+}
diff --git a/formal/promela/models/events/tr-event-mgr-model.h b/formal/promela/models/events/tr-event-mgr-model.h
new file mode 100644
index 00000000..de986f70
--- /dev/null
+++ b/formal/promela/models/events/tr-event-mgr-model.h
@@ -0,0 +1,245 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * @file
+ *
+ * @ingroup RTEMSTestCaseRtemsModelEventsMgr_Run
+ */
+
+/*
+ * 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
+ */
+
+#ifndef _TR_MODEL_EVENTS_MGR_H
+#define _TR_MODEL_EVENTS_MGR_H
+
+#include <rtems.h>
+#include <rtems/score/thread.h>
+
+#include <rtems/test.h>
+#include "ts-config.h"
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+
+/*
+ * Run Setup/Cleanup structs/functions
+ */
+typedef struct {
+  rtems_status_code ( *send )( rtems_id, rtems_event_set ); // copy of the
+                       // corresponding RtemsModelEventsMgr_Run() parameter
+  rtems_status_code ( *receive )
+                    ( rtems_event_set, rtems_option
+                    , rtems_interval, rtems_event_set * ); // copy of the
+                 // corresponding RtemsModelEventsMgr_Run() parameter
+  rtems_event_set ( *get_pending_events )( Thread_Control * ); // copy of the
+                    // corresponding RtemsModelEventsMgr_Run() parameter
+  unsigned int wait_class; // copy of the corresponding
+                           // RtemsModelEventsMgr_Run() parameter
+  int waiting_for_event; // copy of the corresponding
+                         // RtemsModelEventsMgr_Run() parameter
+  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_event_set events_to_send; // events to send for the event send action
+  rtems_status_code send_status; // status of the event send action.
+  rtems_option receive_option_set; // option set used for the event receive action
+  rtems_interval receive_timeout; // timeout used for the event receive action
+  rtems_event_set received_events; // events received by the event receive action
+  rtems_status_code receive_status; // status of the event receive action
+  rtems_event_set unsatisfied_pending; // pending events after an event send action
+                       // which did not satsify the event condition of the receiver
+  Thread_Control *runner_thread; // TCB of the runner task
+  rtems_id runner_id; // ID of the runner task
+  rtems_id worker_id; // task ID of the worker task
+  rtems_id worker_wakeup; // ID of the semaphore used to wake up the worker task
+  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
+} RtemsModelEventsMgr_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 RtemsModelEventsMgr_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, bool wantall );
+
+rtems_id mapid( Context *ctx, int pid ) ;
+
+void checkTaskIs( rtems_id expected_id ) ;
+
+void initialise_pending( rtems_event_set pending[], int max );
+
+void ShowWorkerSemaId( Context *ctx ) ;
+
+void ShowRunnerSemaId( Context *ctx ) ;
+
+void initialise_semaphore( Context *ctx, rtems_id semaphore[] );
+
+void RtemsModelEventsMgr_Setup_Wrap( void *arg ) ;
+
+
+void RtemsModelEventsMgr_Teardown_Wrap( void *arg ) ;
+
+size_t RtemsModelEventsMgr_Scope( void *arg, char *buf, size_t n ) ;
+
+void RtemsModelEventsMgr_Cleanup( RtemsModelEventsMgr_Context *ctx );
+
+/**
+ * @addtogroup RTEMSTestCaseRtemsModelEventsMgr_Run
+ *
+ * @{
+ */
+
+/**
+ * @brief Runs the parameterized test case.
+ *
+ * @param send is the event send handler.
+ *
+ * @param receive is the event receive handler.
+ *
+ * @param get_pending_events is the get pending events handler.
+ *
+ * @param wait_class is the thread wait class.
+ *
+ * @param waiting_for_event is the thread waiting for event state.
+ */
+
+void RtemsModelEventsMgr_Run0(
+  rtems_status_code ( *send )( rtems_id, rtems_event_set ),
+  rtems_status_code ( *receive )( rtems_event_set, rtems_option, rtems_interval, rtems_event_set * ),
+  rtems_event_set (   *get_pending_events )( Thread_Control * ),
+  unsigned int         wait_class,
+  int                  waiting_for_event
+);
+
+void RtemsModelEventsMgr_Run1(
+  rtems_status_code ( *send )( rtems_id, rtems_event_set ),
+  rtems_status_code ( *receive )( rtems_event_set, rtems_option, rtems_interval, rtems_event_set * ),
+  rtems_event_set (   *get_pending_events )( Thread_Control * ),
+  unsigned int         wait_class,
+  int                  waiting_for_event
+);
+
+void RtemsModelEventsMgr_Run2(
+  rtems_status_code ( *send )( rtems_id, rtems_event_set ),
+  rtems_status_code ( *receive )( rtems_event_set, rtems_option, rtems_interval, rtems_event_set * ),
+  rtems_event_set (   *get_pending_events )( Thread_Control * ),
+  unsigned int         wait_class,
+  int                  waiting_for_event
+);
+
+void RtemsModelEventsMgr_Run3(
+  rtems_status_code ( *send )( rtems_id, rtems_event_set ),
+  rtems_status_code ( *receive )( rtems_event_set, rtems_option, rtems_interval, rtems_event_set * ),
+  rtems_event_set (   *get_pending_events )( Thread_Control * ),
+  unsigned int         wait_class,
+  int                  waiting_for_event
+);
+
+void RtemsModelEventsMgr_Run4(
+  rtems_status_code ( *send )( rtems_id, rtems_event_set ),
+  rtems_status_code ( *receive )( rtems_event_set, rtems_option, rtems_interval, rtems_event_set * ),
+  rtems_event_set (   *get_pending_events )( Thread_Control * ),
+  unsigned int         wait_class,
+  int                  waiting_for_event
+);
+
+void RtemsModelEventsMgr_Run5(
+  rtems_status_code ( *send )( rtems_id, rtems_event_set ),
+  rtems_status_code ( *receive )( rtems_event_set, rtems_option, rtems_interval, rtems_event_set * ),
+  rtems_event_set (   *get_pending_events )( Thread_Control * ),
+  unsigned int         wait_class,
+  int                  waiting_for_event
+);
+
+void RtemsModelEventsMgr_Run6(
+  rtems_status_code ( *send )( rtems_id, rtems_event_set ),
+  rtems_status_code ( *receive )( rtems_event_set, rtems_option, rtems_interval, rtems_event_set * ),
+  rtems_event_set (   *get_pending_events )( Thread_Control * ),
+  unsigned int         wait_class,
+  int                  waiting_for_event
+);
+
+void RtemsModelEventsMgr_Run7(
+  rtems_status_code ( *send )( rtems_id, rtems_event_set ),
+  rtems_status_code ( *receive )( rtems_event_set, rtems_option, rtems_interval, rtems_event_set * ),
+  rtems_event_set (   *get_pending_events )( Thread_Control * ),
+  unsigned int         wait_class,
+  int                  waiting_for_event
+);
+
+void RtemsModelEventsMgr_Run8(
+  rtems_status_code ( *send )( rtems_id, rtems_event_set ),
+  rtems_status_code ( *receive )( rtems_event_set, rtems_option, rtems_interval, rtems_event_set * ),
+  rtems_event_set (   *get_pending_events )( Thread_Control * ),
+  unsigned int         wait_class,
+  int                  waiting_for_event
+);
+
+/** @} */
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif /* _TR_EVENT_SEND_RECEIVE_H */
-- 
2.37.1 (Apple Git-137.1)




More information about the devel mailing list