Detailed Description

Overview

This plugin extends libFAUDES to model timed automata as discussed by R. Alur and D.L. Dill. It defines a class to represent time constraints and attribute classes to model guards, invariants and clocksets. Functionality is restricted to basic maintenance inclusive file IO and parallel composition. The motivation of this plugin is to extend the expressiveness of plant and controller models for simulation. It forms the basis for both, our interpreter (aka simulator) as well an Berno Schlein's IEC code generator.

Literature:
R. Alur, D.L. Dill, A Theory of Timed Automata, Theoretical Computer Science, vol 126, pp 183-235, 1994.

License

The current implementation of the timed plugin is a re-design based on Berno Schlein's student projects in the course of migrating from libFAUDES 1.0 to 2.xx. It is distributed with libFAUDES and under the terms of the LGPL.

Classes
class	faudes::AttributeTimedTrans
	Transition Attribute with guard and resets. More...

class	faudes::AttributeTimedState
	State attribute with invariant. More...

class	faudes::AttributeTimedGlobal
	Globat attribute with clockset. More...

class	faudes::TtGenerator< GlobalAttr, StateAttr, EventAttr, TransAttr >
	Generator with timing extensions. More...

class	faudes::ClockSet
	Container class to model a set of clocks. More...

class	faudes::ElemConstraint
	Model of an elementary clock constraint formula. More...

class	faudes::TimeConstraint
	A TimeConstraint is a set of elementary clock constraints. More...

class	faudes::Time
	Type to represent time. More...

class	faudes::TimeInterval
	Model of a time interval. More...

Functions
template<class GlobalAttr1 , class StateAttr1 , class EventAttr1 , class TransAttr1 , class GlobalAttr2 , class StateAttr2 , class EventAttr2 , class TransAttr2 , class GlobalAttrR , class StateAttrR , class EventAttrR , class TransAttrR >
void	faudes::TParallel (const TGEN1 &rGen1, const TGEN2 &rGen2, TGENR &rResGen)
	Parallel composition of timed generators. More...

template<class GlobalAttr1 , class StateAttr1 , class EventAttr1 , class TransAttr1 , class GlobalAttr2 , class StateAttr2 , class EventAttr2 , class TransAttr2 , class GlobalAttrR , class StateAttrR , class EventAttrR , class TransAttrR >
void	faudes::TParallel (const TGEN1 &rGen1, const TGEN2 &rGen2, std::map< std::pair< Idx, Idx >, Idx > &rReverseCompositionMap, TGENR &rResGen)
	Parallel composition of timed generators. More...

Function Documentation

◆ TParallel() [1/2]

template<class GlobalAttr1 , class StateAttr1 , class EventAttr1 , class TransAttr1 , class GlobalAttr2 , class StateAttr2 , class EventAttr2 , class TransAttr2 , class GlobalAttrR , class StateAttrR , class EventAttrR , class TransAttrR >

void faudes::TParallel	(	const TGEN1 &	rGen1,
		const TGEN2 &	rGen2,
		std::map< std::pair< Idx, Idx >, Idx > &	rReverseCompositionMap,
		TGENR &	rResGen
	)

Parallel composition of timed generators.

Arguments rGen1 and rGen2 are assumed to have disjoind clocksets. This implementation considers accessible states only.

Technically, this function is a template, but timed attribute interfaces are assumed. This version fills given reverse composition map with indices.

Parameters

rGen1	First generator
rGen2	Second generator
rReverseCompositionMap	Reverse composition map (map< pair<Idx,Idx>, Idx>)
rResGen	Reference to resulting parallel composition generator

Definition at line 97 of file tp_tparallel.h.

◆ TParallel() [2/2]