Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revisionBoth sides next revision | ||
alvis:modelstate [2015/12/01 12:53] marcin | — (current) | ||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Model state ====== | ||
- | {{ : | ||
- | |||
- | |||
- | **Definition 1.** A **state** of a model A=(D,B,α0), where D=(A,C,σ) and A={X1,...,Xn} is a tuple | ||
- | |||
- | S=(S(X1),…,S(Xn)). | ||
- | |||
- | **Definition 2.** The **initial state** is defined as follows: | ||
- | * // | ||
- | * // | ||
- | * // | ||
- | * // | ||
- | * // | ||
- | * // | ||
- | * For any agent //X//, // | ||
- | |||
- | ===== Example: Sender-Buffer-Receiver system ===== | ||
- | |||
- | {{ : | ||
- | |||
- | < | ||
- | agent Sender { | ||
- | loop { -- 1 | ||
- | out put; -- 2 | ||
- | } | ||
- | } | ||
- | |||
- | agent Buffer { | ||
- | i :: Int = 0; | ||
- | proc (i == 0) put { | ||
- | in put; -- 1 | ||
- | i = 1; -- 2 | ||
- | } | ||
- | proc (i /= 0) get { | ||
- | out get; -- 3 | ||
- | i = 0; -- 4 | ||
- | } | ||
- | } | ||
- | |||
- | agent Receiver { | ||
- | loop { -- 1 | ||
- | in get; -- 2 | ||
- | } | ||
- | } | ||
- | </ | ||
- | |||
- | |||
- | **Initial state:** | ||
- | S_0 = ((X, | ||
- | |||
- | **See also: [[: | ||
- | |||
- | **[[: |