Priorities PlugIn

The priorities plug-in addresses systems with prioritised events. The main purpose is to provide an implementation of the algorithm proposed in [PEV1] and [PEV2] and which extends earlier work [C4] to prioritised events. We briefly outline the context and refer to [PEV1] for further details.

Consider an overall system, composed of a number of generators G1, G2 ... Gn with the common synchronisation of shared events. This establishes the overall alphabet Sigma_all; i.e., the set of all events relevant to either generator under consideration. Each event o ∈ Sigma_all is asigned a non-negative integer to indicate its execution pririty; i.e., we have a map prio\ : Sigma_all→N. as a global entity. Thia map is implemented by the faudes type EventPriorities. It provides access to the individual priorituies and some auxiliar functions, e.g., finding minimum and maximum priorities.

Coming back to the composed system, at any instance of physical time, there is a set of enabled events. Among the enabled events, those of higher priority preempt those of lower priority; i.e., only those of highest priority win the race. A typical application scenario are discrete-event dynamics implemented by a numer of functions in PLC code; actuators can be triggered immediately, while the PLC needs to wait for sensors to report events.

For the trivial case of a system composed of only one component G1, i.e., n = 1, the effect of prioritised events is implemented by the so called shaping operator.. It iterates over all states and removes any outgoing transitions that are labled with some event, that is preempted by another event that is of higher priority. The shaping operator is implemented by the faudes function ShapePriorities

As it happens, the shaping operator does not commute with synchronous composition. In order to evaluate blockingness for a non-trivial composed system, one would naively first compute the ordinary parallel composition, then apply the shaping operator, and finally test for the existence of blocking states. Computaional efficiency can be substantially improved by the compositional approach reported in [PEV1]. Here, the composition of individual components alternates with so called conflict preservin abstractions. An implementation of this method is provided by IsPNonblocking.

This plug-in comes with the scalable conveyor belt example reported in [REV1]; see the tutorials pev_2_verify and pev_3_verfair.

EventPriorities

Alphabet with per event priority attribute.

Detailed description:

The faudes type EventPriorities represents an alphabet with per event priorities. I.e., each event is associatyed with a non-negative integer which indicates execution priority. Events with a higher priority preempt those of lower priority. See also ShapePriorities.

Note. The literature [PEV1] refers to ordinal numbers for priorities, e.g., 1st priority preemts 2nd priority. This turned out counter-intuitive in practice and is not consistent with the priorities used in the Simulator-PlugIn or CompileDES. Thereforr, the current implementation goes by the more common order the higher the figure, the higher the priority; e.g. priority 5 preempts priority 4.

Token-IO is strict XML only. Example: 

<EventPriorities name="aigma_prio">
% event alpha with priority 2
<Event name="alpha">
<Priority value="2"/>
</Event>
% event beta with default priority 0
<Event name="bate"/>
...
</EventPriorities>

ShapePriorities

Shape a generator by prioritiesing events.

Signature:

ShapePriorities(+InOut+ Generator G, +In+ EventPriorities Prios)

Detailed description:

The function ShapePriorities implements the semantics of prioritised events by removing all transitions which are effectively preempted by a higher priority event.

IsPNonblocking

Test for nonblockingness with prioritiesed events.

Signature:

IsPNonblocking(+In+ GeneratorVector G, +In+ EventPriorities Prios, +Out+ Boolean BRes)

Detailed description:

Priorities effect the non-blockingness of composed generators. Specifically, shaping does not commute with parallel composition. Thus, the naive way to test for conflicts in a composed system is to first obtain a monolitic representation, then to apply the shaping operatior, and finally to test for blocking states. In contrast, the function IsPNonblocking implements a compositional approach and aims for relevant computational benefits; see also [PEV1]. The example discussed in the cited literature is provided as tutorial pev_2_verify, both, in a C++ and a Lua version.

Literature

[PEV1] Y. Tang, T. Moor: Compositional verification of non-blockingness with prioritised events, 16th IFAC Workshop on Discrete Event Systems (WODES), 2022.

[PEV2] Y. Tang, T. Moor: Compositional non-blockingness verification of finite automata with prioritised events, Discrete-Event Dynamic Systems, 2024.

libFAUDES 2.33a --- 2025.05.02 --- with "synthesis-observer-observability-diagnosis-hiosys-iosystem-multitasking-coordinationcontrol-timed-simulator-iodevice-priorities-luabindings-hybrid-example-pybindings"

>>