Back to home page

LXR

 
 

    


File indexing completed on 2025-05-11 08:24:53

0001 /* SPDX-License-Identifier: BSD-2-Clause */
0002 
0003 /**
0004  * @file
0005  *
0006  * @ingroup ScoreMtxReqSeizeTry
0007  */
0008 
0009 /*
0010  * Copyright (C) 2021 embedded brains GmbH & Co. KG
0011  *
0012  * Redistribution and use in source and binary forms, with or without
0013  * modification, are permitted provided that the following conditions
0014  * are met:
0015  * 1. Redistributions of source code must retain the above copyright
0016  *    notice, this list of conditions and the following disclaimer.
0017  * 2. Redistributions in binary form must reproduce the above copyright
0018  *    notice, this list of conditions and the following disclaimer in the
0019  *    documentation and/or other materials provided with the distribution.
0020  *
0021  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
0022  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
0023  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
0024  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
0025  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
0026  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
0027  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
0028  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
0029  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
0030  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
0031  * POSSIBILITY OF SUCH DAMAGE.
0032  */
0033 
0034 /*
0035  * This file is part of the RTEMS quality process and was automatically
0036  * generated.  If you find something that needs to be fixed or
0037  * worded better please post a report or patch to an RTEMS mailing list
0038  * or raise a bug report:
0039  *
0040  * https://www.rtems.org/bugs.html
0041  *
0042  * For information on updating and regenerating please refer to the How-To
0043  * section in the Software Requirements Engineering chapter of the
0044  * RTEMS Software Engineering manual.  The manual is provided as a part of
0045  * a release.  For development sources please refer to the online
0046  * documentation at:
0047  *
0048  * https://docs.rtems.org
0049  */
0050 
0051 #ifdef HAVE_CONFIG_H
0052 #include "config.h"
0053 #endif
0054 
0055 #include "tr-mtx-seize-try.h"
0056 
0057 #include <rtems/test.h>
0058 
0059 /**
0060  * @defgroup ScoreMtxReqSeizeTry spec:/score/mtx/req/seize-try
0061  *
0062  * @ingroup TestsuitesValidationNoClock0
0063  *
0064  * @{
0065  */
0066 
0067 typedef struct {
0068   uint16_t Skip : 1;
0069   uint16_t Pre_Protocol_NA : 1;
0070   uint16_t Pre_Discipline_NA : 1;
0071   uint16_t Pre_Recursive_NA : 1;
0072   uint16_t Pre_Owner_NA : 1;
0073   uint16_t Pre_Priority_NA : 1;
0074   uint16_t Post_Status : 3;
0075   uint16_t Post_Owner : 2;
0076   uint16_t Post_Priority : 2;
0077 } ScoreMtxReqSeizeTry_Entry;
0078 
0079 /**
0080  * @brief Test context for spec:/score/mtx/req/seize-try test case.
0081  */
0082 typedef struct {
0083   /**
0084    * @brief If this member is true, then the calling thread shall be the owner
0085    *   of the mutex.
0086    */
0087   bool owner_caller;
0088 
0089   /**
0090    * @brief If this member is true, then a thread other than the calling thread
0091    *   shall be the owner of the mutex.
0092    */
0093   bool owner_other;
0094 
0095   /**
0096    * @brief This member contains the current priority of the calling thread
0097    *   before the directive call.
0098    */
0099   rtems_task_priority priority_before;
0100 
0101   /**
0102    * @brief This member contains the owner of the mutex after the directive
0103    *   call.
0104    */
0105   const rtems_tcb *owner_after;
0106 
0107   /**
0108    * @brief This member contains the current priority of the calling thread
0109    *   after the directive call.
0110    */
0111   rtems_task_priority priority_after;
0112 
0113   /**
0114    * @brief This member contains a copy of the corresponding
0115    *   ScoreMtxReqSeizeTry_Run() parameter.
0116    */
0117   TQMtxContext *tq_ctx;
0118 
0119   struct {
0120     /**
0121      * @brief This member defines the pre-condition indices for the next
0122      *   action.
0123      */
0124     size_t pci[ 5 ];
0125 
0126     /**
0127      * @brief This member defines the pre-condition states for the next action.
0128      */
0129     size_t pcs[ 5 ];
0130 
0131     /**
0132      * @brief If this member is true, then the test action loop is executed.
0133      */
0134     bool in_action_loop;
0135 
0136     /**
0137      * @brief This member contains the next transition map index.
0138      */
0139     size_t index;
0140 
0141     /**
0142      * @brief This member contains the current transition map entry.
0143      */
0144     ScoreMtxReqSeizeTry_Entry entry;
0145 
0146     /**
0147      * @brief If this member is true, then the current transition variant
0148      *   should be skipped.
0149      */
0150     bool skip;
0151   } Map;
0152 } ScoreMtxReqSeizeTry_Context;
0153 
0154 static ScoreMtxReqSeizeTry_Context
0155   ScoreMtxReqSeizeTry_Instance;
0156 
0157 static const char * const ScoreMtxReqSeizeTry_PreDesc_Protocol[] = {
0158   "Ceiling",
0159   "MrsP",
0160   "Other",
0161   "NA"
0162 };
0163 
0164 static const char * const ScoreMtxReqSeizeTry_PreDesc_Discipline[] = {
0165   "FIFO",
0166   "Priority",
0167   "NA"
0168 };
0169 
0170 static const char * const ScoreMtxReqSeizeTry_PreDesc_Recursive[] = {
0171   "Allowed",
0172   "Unavailable",
0173   "Deadlock",
0174   "NA"
0175 };
0176 
0177 static const char * const ScoreMtxReqSeizeTry_PreDesc_Owner[] = {
0178   "None",
0179   "Caller",
0180   "Other",
0181   "NA"
0182 };
0183 
0184 static const char * const ScoreMtxReqSeizeTry_PreDesc_Priority[] = {
0185   "High",
0186   "Equal",
0187   "Low",
0188   "NA"
0189 };
0190 
0191 static const char * const * const ScoreMtxReqSeizeTry_PreDesc[] = {
0192   ScoreMtxReqSeizeTry_PreDesc_Protocol,
0193   ScoreMtxReqSeizeTry_PreDesc_Discipline,
0194   ScoreMtxReqSeizeTry_PreDesc_Recursive,
0195   ScoreMtxReqSeizeTry_PreDesc_Owner,
0196   ScoreMtxReqSeizeTry_PreDesc_Priority,
0197   NULL
0198 };
0199 
0200 typedef ScoreMtxReqSeizeTry_Context Context;
0201 
0202 static Status_Control Status( const Context *ctx, Status_Control status )
0203 {
0204   return TQConvertStatus( &ctx->tq_ctx->base, status );
0205 }
0206 
0207 static bool IsEnqueueStatus( const Context *ctx, Status_Control expected )
0208 {
0209   return ctx->tq_ctx->base.status[ TQ_BLOCKER_A ] == Status( ctx, expected );
0210 }
0211 
0212 static void Action( Context *ctx )
0213 {
0214   TQSetScheduler(
0215     &ctx->tq_ctx->base,
0216     TQ_BLOCKER_A,
0217     SCHEDULER_A_ID,
0218     PRIO_VERY_HIGH
0219   );
0220 
0221   if ( ctx->owner_caller ) {
0222     TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_ENQUEUE );
0223   } else if ( ctx->owner_other ) {
0224     TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_B, TQ_EVENT_ENQUEUE );
0225   }
0226 
0227   TQSetPriority( &ctx->tq_ctx->base, TQ_BLOCKER_A, ctx->priority_before );
0228   TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_ENQUEUE );
0229   ctx->owner_after = TQGetOwner( &ctx->tq_ctx->base );
0230   ctx->priority_after = TQGetPriority( &ctx->tq_ctx->base, TQ_BLOCKER_A );
0231 
0232   if ( ctx->owner_caller ) {
0233     TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_SURRENDER );
0234   } else if ( ctx->owner_other ) {
0235     TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_B, TQ_EVENT_SURRENDER );
0236   }
0237 
0238   if ( IsEnqueueStatus( ctx, STATUS_SUCCESSFUL ) ) {
0239     TQSend( &ctx->tq_ctx->base, TQ_BLOCKER_A, TQ_EVENT_SURRENDER );
0240   }
0241 }
0242 
0243 static void ActionSticky( Context *ctx )
0244 {
0245   TQSetScheduler(
0246     &ctx->tq_ctx->base,
0247     TQ_BLOCKER_A,
0248     SCHEDULER_B_ID,
0249     PRIO_VERY_HIGH
0250   );
0251 
0252   if ( ctx->owner_caller ) {
0253     TQSendAndSynchronizeRunner(
0254       &ctx->tq_ctx->base,
0255       TQ_BLOCKER_A,
0256       TQ_EVENT_ENQUEUE
0257     );
0258   } else if ( ctx->owner_other ) {
0259     SetSelfScheduler( SCHEDULER_B_ID, PRIO_ULTRA_HIGH );
0260     TQSendAndSynchronizeRunner(
0261       &ctx->tq_ctx->base,
0262       TQ_BLOCKER_B,
0263       TQ_EVENT_ENQUEUE
0264     );
0265     SetSelfScheduler( SCHEDULER_A_ID, PRIO_ULTRA_HIGH );
0266   }
0267 
0268   TQSetPriority( &ctx->tq_ctx->base, TQ_BLOCKER_A, ctx->priority_before );
0269   TQClearDone( &ctx->tq_ctx->base, TQ_BLOCKER_A );
0270   TQSendAndWaitForExecutionStopOrIntendToBlock(
0271     &ctx->tq_ctx->base,
0272     TQ_BLOCKER_A,
0273     TQ_EVENT_ENQUEUE
0274   );
0275   ctx->owner_after = TQGetOwner( &ctx->tq_ctx->base );
0276   ctx->priority_after = TQGetPriority( &ctx->tq_ctx->base, TQ_BLOCKER_A );
0277 
0278   if ( ctx->owner_caller ) {
0279     TQSendAndSynchronizeRunner(
0280       &ctx->tq_ctx->base,
0281       TQ_BLOCKER_A,
0282       TQ_EVENT_SURRENDER
0283     );
0284   } else if ( ctx->owner_other ) {
0285     SetSelfScheduler( SCHEDULER_B_ID, PRIO_ULTRA_HIGH );
0286     TQSendAndSynchronizeRunner(
0287       &ctx->tq_ctx->base,
0288       TQ_BLOCKER_B,
0289       TQ_EVENT_SURRENDER
0290     );
0291     SetSelfScheduler( SCHEDULER_A_ID, PRIO_NORMAL );
0292   }
0293 
0294   TQWaitForDone( &ctx->tq_ctx->base, TQ_BLOCKER_A );
0295 
0296   if ( IsEnqueueStatus( ctx, STATUS_SUCCESSFUL ) ) {
0297     TQSendAndSynchronizeRunner(
0298       &ctx->tq_ctx->base,
0299       TQ_BLOCKER_A,
0300       TQ_EVENT_SURRENDER
0301     );
0302   }
0303 }
0304 
0305 static void ScoreMtxReqSeizeTry_Pre_Protocol_Prepare(
0306   ScoreMtxReqSeizeTry_Context     *ctx,
0307   ScoreMtxReqSeizeTry_Pre_Protocol state
0308 )
0309 {
0310   switch ( state ) {
0311     case ScoreMtxReqSeizeTry_Pre_Protocol_Ceiling: {
0312       /*
0313        * Where the mutex uses the priority ceiling locking protocol.
0314        */
0315       if (
0316         ctx->tq_ctx->priority_ceiling == PRIO_INVALID ||
0317         ctx->tq_ctx->base.enqueue_variant == TQ_ENQUEUE_STICKY
0318       ) {
0319         ctx->Map.skip = true;
0320       }
0321       break;
0322     }
0323 
0324     case ScoreMtxReqSeizeTry_Pre_Protocol_MrsP: {
0325       /*
0326        * Where the mutex uses the MrsP locking protocol.
0327        */
0328       if (
0329         ctx->tq_ctx->priority_ceiling == PRIO_INVALID ||
0330         ctx->tq_ctx->base.enqueue_variant != TQ_ENQUEUE_STICKY
0331       ) {
0332         ctx->Map.skip = true;
0333       }
0334       break;
0335     }
0336 
0337     case ScoreMtxReqSeizeTry_Pre_Protocol_Other: {
0338       /*
0339        * Where the mutex does not use the priority ceiling or MrsP locking
0340        * protocol.
0341        */
0342       if ( ctx->tq_ctx->priority_ceiling != PRIO_INVALID ) {
0343         ctx->Map.skip = true;
0344       }
0345       break;
0346     }
0347 
0348     case ScoreMtxReqSeizeTry_Pre_Protocol_NA:
0349       break;
0350   }
0351 }
0352 
0353 static void ScoreMtxReqSeizeTry_Pre_Discipline_Prepare(
0354   ScoreMtxReqSeizeTry_Context       *ctx,
0355   ScoreMtxReqSeizeTry_Pre_Discipline state
0356 )
0357 {
0358   switch ( state ) {
0359     case ScoreMtxReqSeizeTry_Pre_Discipline_FIFO: {
0360       /*
0361        * Where the thread queue of the mutex uses the FIFO discipline.
0362        */
0363       if ( ctx->tq_ctx->base.discipline != TQ_FIFO ) {
0364         ctx->Map.skip = true;
0365       }
0366       break;
0367     }
0368 
0369     case ScoreMtxReqSeizeTry_Pre_Discipline_Priority: {
0370       /*
0371        * Where the thread queue of the mutex uses the priority discipline.
0372        */
0373       if ( ctx->tq_ctx->base.discipline != TQ_PRIORITY ) {
0374         ctx->Map.skip = true;
0375       }
0376       break;
0377     }
0378 
0379     case ScoreMtxReqSeizeTry_Pre_Discipline_NA:
0380       break;
0381   }
0382 }
0383 
0384 static void ScoreMtxReqSeizeTry_Pre_Recursive_Prepare(
0385   ScoreMtxReqSeizeTry_Context      *ctx,
0386   ScoreMtxReqSeizeTry_Pre_Recursive state
0387 )
0388 {
0389   switch ( state ) {
0390     case ScoreMtxReqSeizeTry_Pre_Recursive_Allowed: {
0391       /*
0392        * Where a recursive seize of the mutex is allowed.
0393        */
0394       if ( ctx->tq_ctx->recursive != TQ_MTX_RECURSIVE_ALLOWED ) {
0395         ctx->Map.skip = true;
0396       }
0397       break;
0398     }
0399 
0400     case ScoreMtxReqSeizeTry_Pre_Recursive_Unavailable: {
0401       /*
0402        * Where a recursive seize of the mutex results in an unavailable status.
0403        */
0404       if ( ctx->tq_ctx->recursive != TQ_MTX_RECURSIVE_UNAVAILABLE ) {
0405         ctx->Map.skip = true;
0406       }
0407       break;
0408     }
0409 
0410     case ScoreMtxReqSeizeTry_Pre_Recursive_Deadlock: {
0411       /*
0412        * Where a recursive seize of the mutex results in a deadlock status.
0413        */
0414       if ( ctx->tq_ctx->recursive != TQ_MTX_RECURSIVE_DEADLOCK ) {
0415         ctx->Map.skip = true;
0416       }
0417       break;
0418     }
0419 
0420     case ScoreMtxReqSeizeTry_Pre_Recursive_NA:
0421       break;
0422   }
0423 }
0424 
0425 static void ScoreMtxReqSeizeTry_Pre_Owner_Prepare(
0426   ScoreMtxReqSeizeTry_Context  *ctx,
0427   ScoreMtxReqSeizeTry_Pre_Owner state
0428 )
0429 {
0430   switch ( state ) {
0431     case ScoreMtxReqSeizeTry_Pre_Owner_None: {
0432       /*
0433        * While the mutex has no owner.
0434        */
0435       /* This is the default */
0436       break;
0437     }
0438 
0439     case ScoreMtxReqSeizeTry_Pre_Owner_Caller: {
0440       /*
0441        * While the owner of the mutex is the calling thread.
0442        */
0443       ctx->owner_caller = true;
0444       break;
0445     }
0446 
0447     case ScoreMtxReqSeizeTry_Pre_Owner_Other: {
0448       /*
0449        * While the owner of the mutex is a thread other than the calling
0450        * thread.
0451        */
0452       ctx->owner_other = true;
0453       break;
0454     }
0455 
0456     case ScoreMtxReqSeizeTry_Pre_Owner_NA:
0457       break;
0458   }
0459 }
0460 
0461 static void ScoreMtxReqSeizeTry_Pre_Priority_Prepare(
0462   ScoreMtxReqSeizeTry_Context     *ctx,
0463   ScoreMtxReqSeizeTry_Pre_Priority state
0464 )
0465 {
0466   switch ( state ) {
0467     case ScoreMtxReqSeizeTry_Pre_Priority_High: {
0468       /*
0469        * While the calling thread has a current priority higher than the
0470        * priority ceiling.
0471        */
0472       ctx->priority_before = ctx->tq_ctx->priority_ceiling - 1;
0473       break;
0474     }
0475 
0476     case ScoreMtxReqSeizeTry_Pre_Priority_Equal: {
0477       /*
0478        * While the calling thread has a current priority equal to the priority
0479        * ceiling.
0480        */
0481       ctx->priority_before = ctx->tq_ctx->priority_ceiling;
0482       break;
0483     }
0484 
0485     case ScoreMtxReqSeizeTry_Pre_Priority_Low: {
0486       /*
0487        * While the calling thread has a current priority lower than the
0488        * priority ceiling.
0489        */
0490       ctx->priority_before = ctx->tq_ctx->priority_ceiling + 1;
0491       break;
0492     }
0493 
0494     case ScoreMtxReqSeizeTry_Pre_Priority_NA:
0495       break;
0496   }
0497 }
0498 
0499 static void ScoreMtxReqSeizeTry_Post_Status_Check(
0500   ScoreMtxReqSeizeTry_Context    *ctx,
0501   ScoreMtxReqSeizeTry_Post_Status state
0502 )
0503 {
0504   switch ( state ) {
0505     case ScoreMtxReqSeizeTry_Post_Status_Ok: {
0506       /*
0507        * The return status of the directive call shall be derived from
0508        * STATUS_SUCCESSFUL.
0509        */
0510       T_true( IsEnqueueStatus( ctx, STATUS_SUCCESSFUL ) );
0511       break;
0512     }
0513 
0514     case ScoreMtxReqSeizeTry_Post_Status_MutexCeilingViolated: {
0515       /*
0516        * The return status of the directive call shall be derived from
0517        * STATUS_MUTEX_CEILING_VIOLATED.
0518        */
0519       T_true( IsEnqueueStatus( ctx, STATUS_MUTEX_CEILING_VIOLATED ) );
0520       break;
0521     }
0522 
0523     case ScoreMtxReqSeizeTry_Post_Status_Deadlock: {
0524       /*
0525        * The return status of the directive call shall be derived from
0526        * STATUS_DEADLOCK.
0527        */
0528       T_true( IsEnqueueStatus( ctx, STATUS_DEADLOCK ) );
0529       break;
0530     }
0531 
0532     case ScoreMtxReqSeizeTry_Post_Status_Unavailable: {
0533       /*
0534        * The return status of the directive call shall be derived from
0535        * STATUS_UNAVAILABLE.
0536        */
0537       T_true( IsEnqueueStatus( ctx, STATUS_UNAVAILABLE ) );
0538       break;
0539     }
0540 
0541     case ScoreMtxReqSeizeTry_Post_Status_NA:
0542       break;
0543   }
0544 }
0545 
0546 static void ScoreMtxReqSeizeTry_Post_Owner_Check(
0547   ScoreMtxReqSeizeTry_Context   *ctx,
0548   ScoreMtxReqSeizeTry_Post_Owner state
0549 )
0550 {
0551   switch ( state ) {
0552     case ScoreMtxReqSeizeTry_Post_Owner_Other: {
0553       /*
0554        * The owner of the mutex shall not be modified.
0555        */
0556       T_eq_ptr(
0557         ctx->owner_after,
0558         ctx->tq_ctx->base.worker_tcb[ TQ_BLOCKER_B ]
0559       );
0560       break;
0561     }
0562 
0563     case ScoreMtxReqSeizeTry_Post_Owner_Caller: {
0564       /*
0565        * The owner of the mutex shall be the calling thread.
0566        */
0567       T_eq_ptr(
0568         ctx->owner_after,
0569         ctx->tq_ctx->base.worker_tcb[ TQ_BLOCKER_A ]
0570       );
0571       break;
0572     }
0573 
0574     case ScoreMtxReqSeizeTry_Post_Owner_None: {
0575       /*
0576        * The mutex shall have no owner.
0577        */
0578       T_null( ctx->owner_after );
0579       break;
0580     }
0581 
0582     case ScoreMtxReqSeizeTry_Post_Owner_NA:
0583       break;
0584   }
0585 }
0586 
0587 static void ScoreMtxReqSeizeTry_Post_Priority_Check(
0588   ScoreMtxReqSeizeTry_Context      *ctx,
0589   ScoreMtxReqSeizeTry_Post_Priority state
0590 )
0591 {
0592   switch ( state ) {
0593     case ScoreMtxReqSeizeTry_Post_Priority_Nop: {
0594       /*
0595        * The priorities of the calling thread shall not be modified.
0596        */
0597       T_eq_u32( ctx->priority_after, ctx->priority_before );
0598       break;
0599     }
0600 
0601     case ScoreMtxReqSeizeTry_Post_Priority_Ceiling: {
0602       /*
0603        * The calling thread shall use the priority ceiling of the mutex.
0604        */
0605       T_eq_u32( ctx->priority_after, ctx->tq_ctx->priority_ceiling );
0606       break;
0607     }
0608 
0609     case ScoreMtxReqSeizeTry_Post_Priority_NA:
0610       break;
0611   }
0612 }
0613 
0614 static void ScoreMtxReqSeizeTry_Prepare( ScoreMtxReqSeizeTry_Context *ctx )
0615 {
0616   ctx->owner_caller = false;
0617   ctx->owner_other = false;
0618   ctx->priority_before = PRIO_VERY_HIGH;
0619 }
0620 
0621 static void ScoreMtxReqSeizeTry_Action( ScoreMtxReqSeizeTry_Context *ctx )
0622 {
0623   TQSetScheduler(
0624     &ctx->tq_ctx->base,
0625     TQ_BLOCKER_B,
0626     SCHEDULER_A_ID,
0627     PRIO_VERY_HIGH
0628   );
0629 
0630   if ( ctx->tq_ctx->base.enqueue_variant == TQ_ENQUEUE_STICKY ) {
0631     ActionSticky( ctx );
0632   } else {
0633     Action( ctx );
0634   }
0635 }
0636 
0637 static const ScoreMtxReqSeizeTry_Entry
0638 ScoreMtxReqSeizeTry_Entries[] = {
0639   { 1, 0, 0, 0, 0, 0, ScoreMtxReqSeizeTry_Post_Status_NA,
0640     ScoreMtxReqSeizeTry_Post_Owner_NA, ScoreMtxReqSeizeTry_Post_Priority_NA },
0641   { 0, 0, 0, 0, 0, 1, ScoreMtxReqSeizeTry_Post_Status_Ok,
0642     ScoreMtxReqSeizeTry_Post_Owner_Caller,
0643     ScoreMtxReqSeizeTry_Post_Priority_Nop },
0644   { 0, 0, 0, 0, 0, 0, ScoreMtxReqSeizeTry_Post_Status_Unavailable,
0645     ScoreMtxReqSeizeTry_Post_Owner_Other, ScoreMtxReqSeizeTry_Post_Priority_Nop },
0646   { 0, 0, 0, 0, 0, 1, ScoreMtxReqSeizeTry_Post_Status_Unavailable,
0647     ScoreMtxReqSeizeTry_Post_Owner_Other, ScoreMtxReqSeizeTry_Post_Priority_Nop },
0648   { 0, 0, 0, 0, 0, 0, ScoreMtxReqSeizeTry_Post_Status_Ok,
0649     ScoreMtxReqSeizeTry_Post_Owner_Caller,
0650     ScoreMtxReqSeizeTry_Post_Priority_Ceiling },
0651   { 0, 0, 0, 0, 0, 0, ScoreMtxReqSeizeTry_Post_Status_MutexCeilingViolated,
0652     ScoreMtxReqSeizeTry_Post_Owner_None, ScoreMtxReqSeizeTry_Post_Priority_Nop },
0653   { 1, 0, 0, 0, 0, 0, ScoreMtxReqSeizeTry_Post_Status_NA,
0654     ScoreMtxReqSeizeTry_Post_Owner_NA, ScoreMtxReqSeizeTry_Post_Priority_NA },
0655   { 0, 0, 0, 0, 0, 1, ScoreMtxReqSeizeTry_Post_Status_Unavailable,
0656     ScoreMtxReqSeizeTry_Post_Owner_Caller,
0657     ScoreMtxReqSeizeTry_Post_Priority_Nop },
0658   { 0, 0, 0, 0, 0, 1, ScoreMtxReqSeizeTry_Post_Status_Deadlock,
0659     ScoreMtxReqSeizeTry_Post_Owner_Caller,
0660     ScoreMtxReqSeizeTry_Post_Priority_Nop },
0661   { 0, 0, 0, 0, 0, 0, ScoreMtxReqSeizeTry_Post_Status_Ok,
0662     ScoreMtxReqSeizeTry_Post_Owner_Caller,
0663     ScoreMtxReqSeizeTry_Post_Priority_Nop },
0664   { 0, 0, 0, 0, 0, 0, ScoreMtxReqSeizeTry_Post_Status_Unavailable,
0665     ScoreMtxReqSeizeTry_Post_Owner_Caller,
0666     ScoreMtxReqSeizeTry_Post_Priority_Nop },
0667   { 0, 0, 0, 0, 0, 0, ScoreMtxReqSeizeTry_Post_Status_Deadlock,
0668     ScoreMtxReqSeizeTry_Post_Owner_Caller,
0669     ScoreMtxReqSeizeTry_Post_Priority_Nop }
0670 };
0671 
0672 static const uint8_t
0673 ScoreMtxReqSeizeTry_Map[] = {
0674   0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
0675   0, 5, 4, 4, 9, 9, 6, 2, 2, 2, 5, 4, 4, 10, 10, 6, 2, 2, 2, 5, 4, 4, 11, 11,
0676   6, 2, 2, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
0677   0, 0, 0, 0, 0, 5, 4, 4, 9, 9, 6, 2, 2, 2, 5, 4, 4, 10, 10, 6, 2, 2, 2, 5, 4,
0678   4, 11, 11, 6, 2, 2, 2, 1, 1, 1, 1, 1, 1, 3, 3, 3, 1, 1, 1, 7, 7, 7, 3, 3, 3,
0679   1, 1, 1, 8, 8, 8, 3, 3, 3, 1, 1, 1, 1, 1, 1, 3, 3, 3, 1, 1, 1, 7, 7, 7, 3, 3,
0680   3, 1, 1, 1, 8, 8, 8, 3, 3, 3
0681 };
0682 
0683 static size_t ScoreMtxReqSeizeTry_Scope( void *arg, char *buf, size_t n )
0684 {
0685   ScoreMtxReqSeizeTry_Context *ctx;
0686 
0687   ctx = arg;
0688 
0689   if ( ctx->Map.in_action_loop ) {
0690     return T_get_scope( ScoreMtxReqSeizeTry_PreDesc, buf, n, ctx->Map.pcs );
0691   }
0692 
0693   return 0;
0694 }
0695 
0696 static T_fixture ScoreMtxReqSeizeTry_Fixture = {
0697   .setup = NULL,
0698   .stop = NULL,
0699   .teardown = NULL,
0700   .scope = ScoreMtxReqSeizeTry_Scope,
0701   .initial_context = &ScoreMtxReqSeizeTry_Instance
0702 };
0703 
0704 static const uint8_t ScoreMtxReqSeizeTry_Weights[] = {
0705   54, 27, 9, 3, 1
0706 };
0707 
0708 static void ScoreMtxReqSeizeTry_Skip(
0709   ScoreMtxReqSeizeTry_Context *ctx,
0710   size_t                       index
0711 )
0712 {
0713   switch ( index + 1 ) {
0714     case 1:
0715       ctx->Map.pci[ 1 ] = ScoreMtxReqSeizeTry_Pre_Discipline_NA - 1;
0716       /* Fall through */
0717     case 2:
0718       ctx->Map.pci[ 2 ] = ScoreMtxReqSeizeTry_Pre_Recursive_NA - 1;
0719       /* Fall through */
0720     case 3:
0721       ctx->Map.pci[ 3 ] = ScoreMtxReqSeizeTry_Pre_Owner_NA - 1;
0722       /* Fall through */
0723     case 4:
0724       ctx->Map.pci[ 4 ] = ScoreMtxReqSeizeTry_Pre_Priority_NA - 1;
0725       break;
0726   }
0727 }
0728 
0729 static inline ScoreMtxReqSeizeTry_Entry ScoreMtxReqSeizeTry_PopEntry(
0730   ScoreMtxReqSeizeTry_Context *ctx
0731 )
0732 {
0733   size_t index;
0734 
0735   if ( ctx->Map.skip ) {
0736     size_t i;
0737 
0738     ctx->Map.skip = false;
0739     index = 0;
0740 
0741     for ( i = 0; i < 5; ++i ) {
0742       index += ScoreMtxReqSeizeTry_Weights[ i ] * ctx->Map.pci[ i ];
0743     }
0744   } else {
0745     index = ctx->Map.index;
0746   }
0747 
0748   ctx->Map.index = index + 1;
0749 
0750   return ScoreMtxReqSeizeTry_Entries[
0751     ScoreMtxReqSeizeTry_Map[ index ]
0752   ];
0753 }
0754 
0755 static void ScoreMtxReqSeizeTry_SetPreConditionStates(
0756   ScoreMtxReqSeizeTry_Context *ctx
0757 )
0758 {
0759   ctx->Map.pcs[ 0 ] = ctx->Map.pci[ 0 ];
0760   ctx->Map.pcs[ 1 ] = ctx->Map.pci[ 1 ];
0761   ctx->Map.pcs[ 2 ] = ctx->Map.pci[ 2 ];
0762   ctx->Map.pcs[ 3 ] = ctx->Map.pci[ 3 ];
0763 
0764   if ( ctx->Map.entry.Pre_Priority_NA ) {
0765     ctx->Map.pcs[ 4 ] = ScoreMtxReqSeizeTry_Pre_Priority_NA;
0766   } else {
0767     ctx->Map.pcs[ 4 ] = ctx->Map.pci[ 4 ];
0768   }
0769 }
0770 
0771 static void ScoreMtxReqSeizeTry_TestVariant( ScoreMtxReqSeizeTry_Context *ctx )
0772 {
0773   ScoreMtxReqSeizeTry_Pre_Protocol_Prepare( ctx, ctx->Map.pcs[ 0 ] );
0774 
0775   if ( ctx->Map.skip ) {
0776     ScoreMtxReqSeizeTry_Skip( ctx, 0 );
0777     return;
0778   }
0779 
0780   ScoreMtxReqSeizeTry_Pre_Discipline_Prepare( ctx, ctx->Map.pcs[ 1 ] );
0781 
0782   if ( ctx->Map.skip ) {
0783     ScoreMtxReqSeizeTry_Skip( ctx, 1 );
0784     return;
0785   }
0786 
0787   ScoreMtxReqSeizeTry_Pre_Recursive_Prepare( ctx, ctx->Map.pcs[ 2 ] );
0788 
0789   if ( ctx->Map.skip ) {
0790     ScoreMtxReqSeizeTry_Skip( ctx, 2 );
0791     return;
0792   }
0793 
0794   ScoreMtxReqSeizeTry_Pre_Owner_Prepare( ctx, ctx->Map.pcs[ 3 ] );
0795   ScoreMtxReqSeizeTry_Pre_Priority_Prepare( ctx, ctx->Map.pcs[ 4 ] );
0796   ScoreMtxReqSeizeTry_Action( ctx );
0797   ScoreMtxReqSeizeTry_Post_Status_Check( ctx, ctx->Map.entry.Post_Status );
0798   ScoreMtxReqSeizeTry_Post_Owner_Check( ctx, ctx->Map.entry.Post_Owner );
0799   ScoreMtxReqSeizeTry_Post_Priority_Check( ctx, ctx->Map.entry.Post_Priority );
0800 }
0801 
0802 static T_fixture_node ScoreMtxReqSeizeTry_Node;
0803 
0804 static T_remark ScoreMtxReqSeizeTry_Remark = {
0805   .next = NULL,
0806   .remark = "ScoreMtxReqSeizeTry"
0807 };
0808 
0809 void ScoreMtxReqSeizeTry_Run( TQMtxContext *tq_ctx )
0810 {
0811   ScoreMtxReqSeizeTry_Context *ctx;
0812 
0813   ctx = &ScoreMtxReqSeizeTry_Instance;
0814   ctx->tq_ctx = tq_ctx;
0815 
0816   ctx = T_push_fixture(
0817     &ScoreMtxReqSeizeTry_Node,
0818     &ScoreMtxReqSeizeTry_Fixture
0819   );
0820   ctx->Map.in_action_loop = true;
0821   ctx->Map.index = 0;
0822   ctx->Map.skip = false;
0823 
0824   for (
0825     ctx->Map.pci[ 0 ] = ScoreMtxReqSeizeTry_Pre_Protocol_Ceiling;
0826     ctx->Map.pci[ 0 ] < ScoreMtxReqSeizeTry_Pre_Protocol_NA;
0827     ++ctx->Map.pci[ 0 ]
0828   ) {
0829     for (
0830       ctx->Map.pci[ 1 ] = ScoreMtxReqSeizeTry_Pre_Discipline_FIFO;
0831       ctx->Map.pci[ 1 ] < ScoreMtxReqSeizeTry_Pre_Discipline_NA;
0832       ++ctx->Map.pci[ 1 ]
0833     ) {
0834       for (
0835         ctx->Map.pci[ 2 ] = ScoreMtxReqSeizeTry_Pre_Recursive_Allowed;
0836         ctx->Map.pci[ 2 ] < ScoreMtxReqSeizeTry_Pre_Recursive_NA;
0837         ++ctx->Map.pci[ 2 ]
0838       ) {
0839         for (
0840           ctx->Map.pci[ 3 ] = ScoreMtxReqSeizeTry_Pre_Owner_None;
0841           ctx->Map.pci[ 3 ] < ScoreMtxReqSeizeTry_Pre_Owner_NA;
0842           ++ctx->Map.pci[ 3 ]
0843         ) {
0844           for (
0845             ctx->Map.pci[ 4 ] = ScoreMtxReqSeizeTry_Pre_Priority_High;
0846             ctx->Map.pci[ 4 ] < ScoreMtxReqSeizeTry_Pre_Priority_NA;
0847             ++ctx->Map.pci[ 4 ]
0848           ) {
0849             ctx->Map.entry = ScoreMtxReqSeizeTry_PopEntry( ctx );
0850 
0851             if ( ctx->Map.entry.Skip ) {
0852               continue;
0853             }
0854 
0855             ScoreMtxReqSeizeTry_SetPreConditionStates( ctx );
0856             ScoreMtxReqSeizeTry_Prepare( ctx );
0857             ScoreMtxReqSeizeTry_TestVariant( ctx );
0858           }
0859         }
0860       }
0861     }
0862   }
0863 
0864   T_add_remark( &ScoreMtxReqSeizeTry_Remark );
0865   T_pop_fixture();
0866 }
0867 
0868 /** @} */