Sidebar

Main

Internal

Trace:

Differences

This shows you the differences between two versions of the page.

--- alvis:model [2013/12/29 22:00]
marcin
+++ — (current)
@@ Line 1: / Line 1: @@
-====== Formal model definition ======
-An Alvis **model** is defined as shown in Definition 1.
-**Definition 1.** An Alvis **model** is a triple **A** = (//H//, //B//, φ), where:
-  * //H// is a **hierarchical communication diagram**,
-  * //B// is a syntactically correct **code layer**,
-  * φ is a **system layer**.
-Moreover, each non-hierarchical agent //X// belonging to the diagram //H// must be defined in the code layer, and each agent defined in the code layer must belong to the diagram.
-It should be underlined that **currently Alvis Compiler supports α^0 system layer only**.
-Before generation of the Haskell model representation models are transformed into equivalent non-hierarchical form. The transformation applies to the communication diagram only. Thus, from the theoretical point of view, we can consider models defined as **A** = (//D//,//B//,φ), where //D// is a **non-hierarchical communication diagram**.
-**Definition 2.** A **non-hierarchical communication diagram** is a triple //D// = (//A//, //C//, σ), where:
-  * //A// = {X_1,...,X_n} is the set of **agents** consisting of two disjoint sets, //A_A//, //A_P// such that //A// = //A_A// ∪ //A_P//, containing **active** and **passive** agents respectively;
-  * //C// ⊆ //P// × //P//, where //P// is the set of all ports, is the **communication relation**, such that:
-    * a connection cannot be defined between ports of the same agent;
-    * procedure ports are either input or output ones i.e. ports defined as procedures are used to transfer signals (values) either to or from a passive agent;
-    * a connection between an active and a passive agent must be a procedure call;
-    * a connection between two passive agents must be a procedure call from a non-procedure port.
-  * The start function σ makes possible delaying activation of some agents.
-Each element belonging to //C// is called a **connection** or a **communication channel**.
-Names of agents that are initially activated are underlined in a communication diagram.
-**FIXME**
-**[[:alvis:manual|Go back]]**