---
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", ¤t_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", ¤t_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", ¤t_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", ¤t_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)
_______________________________________________
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel
[PATCH 06/18] adds event manager model
andrew.butterfi...@scss.tcd.ie Thu, 22 Dec 2022 03:39:06 -0800
