Priorities Plug-In

Detailed Description

The priorities plug-in addresses systems with prioritised events. Technically, an event priority is a non-negatie integer. Semantically, events of higher priority will preempt any event of lower priority.

As its base API, this plug-in provides

• the template faudes::TpEventSet for an alphabet of prioritised events,
• the template faudes::TpGenerator for a generator with prioritised events, and
• the function faudes::ShapePriorities to implement the premting effect for a given generator. Usage should be fairly intuitive, see also the provided tutorials.

Regarding algorithms, we provide the two function

• faudes::IsPNonconflicting and
• faudes::IsPFNonconflicting Both functions implement a compositional approach to the verfication of non-conflictingness for the parallel composition of multiple components with a global interpretation of preemption by event priorities. Thechnical details have been reported in

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

The code base is Yiheng Tang's original work with some later cos,etic extensions to address consistent integration with libFAUDES and Lua bindings.

License

The priosities plugin is distributed with libFAUDES and under the terms of the LGPL.

Copyright (c) 2024,2025, Yiheng Tang, Thomas Moor.

Classes
class	faudes::AttributePriority
class	faudes::TpEventSet< Attr >

Typedefs
typedef TpEventSet< AttributePriority >	faudes::EventPriorities
typedef TBaseVector< EventSet >	faudes::FairnessConstraints

Functions
void	faudes::ShapePriorities (vGenerator &rGen, const EventPriorities &rPrios)
void	faudes::ShapePriorities (pGenerator &rPGen)
void	faudes::ShapeUpsilon (pGenerator &rPGen, const EventSet &rUpsilon)
void	faudes::ShapePreemption (Generator &rGen, const EventSet &pevs)
bool	faudes::IsPFNonblocking (const GeneratorVector &rGvec, const EventPriorities &rPrios, const std::vector< FairnessConstraints > &rFairVec)
bool	faudes::IsPNonblocking (const GeneratorVector &rGvec, const EventPriorities &rPrios)

Typedef Documentation

EventPriorities

typedef TpEventSet<AttributePriority> faudes::EventPriorities

Convenience typedef for std alphabet with priorities

Definition at line 424 of file pev_priorities.h.

FairnessConstraints

typedef TBaseVector<EventSet> faudes::FairnessConstraints

Convenience typedef for fairness constraints (one EventSet per constraint)

Definition at line 431 of file pev_priorities.h.

Function Documentation

IsPFNonblocking()

FAUDES_API bool faudes::IsPFNonblocking	(	const GeneratorVector &	rGvec,
		const EventPriorities &	rPrios,
		const std::vector< FairnessConstraints > &	rFairVec
	)

Nonconflicting Test

Given a family of generators and global event priorities, decide whether or not the synchronous composition is non-conflicting under event priorisation. This function is a variant of faudes::IsPFNonblocking that addresses a generalised concept of fairness.

Parameters

rGvec	generators to consider
rPrios	global event priosities
rFairVec	one fairness constraint per generator

Returns

true for nonconflicting

Definition at line 2018 of file pev_abstraction.cpp.

IsPNonblocking()

FAUDES_API bool faudes::IsPNonblocking	(	const GeneratorVector &	rGvec,
		const EventPriorities &	rPrios
	)

Nonconflicting Test

Given a family of generators and global event priorities, decide whether or not the synchronous composition is non-conflicting under event priorisation. This functions implements a compositional approach to avoid an explicit representation of the composed overall system.

Parameters

rGvec	generators to consider
rPrevs	global event priosities

Returns

true for nonconflicting

Definition at line 2189 of file pev_abstraction.cpp.

ShapePreemption()

FAUDES_API void faudes::ShapePreemption	(	Generator &	rGen,
		const EventSet &	rPrevs
	)

Shape generator by removing preempted transitions

Parameters

rGen	generator to shape
rPrevs	set of preempting events

Definition at line 909 of file pev_abstraction.cpp.

ShapePriorities() [1/2]

FAUDES_API void faudes::ShapePriorities

(

pGenerator &

rPGen

)

Shape generator by removing transitions that are preempted by higher priority altyernatives.

Parameters

rPGen

generator to shape incl. event priorities

Definition at line 899 of file pev_abstraction.cpp.

ShapePriorities() [2/2]

FAUDES_API void faudes::ShapePriorities	(	vGenerator &	rGen,
		const EventPriorities &	rPrios
	)

Shape generator by removing transitions that are preempted by higher priority altyernatives.

Parameters

rGen	generator to shape
rPrios	event priorities

Definition at line 893 of file pev_abstraction.cpp.

ShapeUpsilon()

FAUDES_API void faudes::ShapeUpsilon	(	pGenerator &	rPGen,
		const EventSet &	rUpsilon
	)

Shape generator by removing transitions that are preempted by higher priority alternatives.

Parameters

rPGen	generator to shape incl. event priorities
rUpsilon	only consider events in Upsilon for shaping

Definition at line 887 of file pev_abstraction.cpp.