Title: Theory / Unimportant / CS / Softw / UPPAAL / new tuto
Tags: récupéré hasNotNewEffectReturnsMeaning FromInstruction computer_to_instruction type declaration hasSeenConjDef seen_description

Instruction: const type var
Page: 2
Meaning: the introduced value is constant
Section: 2.1
Variables: \(C\) a set of clock
Similar to: type var

Typ: int[foo,bar] buz
Meaning: Introduce a variable names buz whose value is between foo and bar. States where buz does not satisfy this constraints are invalid
Page: 2
Section: 2.1

Typ: chan foo
Meaning: Introduce a channel called foo
Page: 6
Section: 2.1

Instruction: broadcast chan foo
Page: 6
Effect: Introduce a broadcasting channel called foo. When !foo is emitted, every foo? firable transitions must be taken
Section: 2.1

Instruction: urgent chan
Page: 6
Meaning: The channel declared after must be taken without delay
Section: 2.1
Similar to: chan

Instruction: urgent location
Page: 6
Effect: Equivalent to adding a clock \(x\) and the invariant constraint x<=0
Section: 2.1

Name: Committed locations
Definition: A location where an edge taken must leave at least one committed locations
Page: 6
Section: 2.1

Typ: foo[n]
Meaning: The type of an array with n elements of type foo
Page: 6
Section: 2.1
Variables: foo a type

Typ: struct
Meaning: Introduce a struct construct like in C
Page: 6
Section: 2.1

Typ: typedef
Meaning: Introduce a custom type like in C
Page: 6
Section: 2.1

Instruction: A comma separated list of name: type
Page: 6
Section: 2.1
Name: Select

Name: Guard
Definition: it is side-effect free
Page: 6
Section: 2.1
Context: Uppaal
Definition2: it evaluates to a boolean
Conjdef: particular expression satisfying the following conditions:
Definition3: only clocks, integer variables, and constants are referenced (or arrays of these types); clocks and clock differences are only compared to integer expressions;

Name: Synchronisation
Definition: Either on the form Expression! or Expression? or is an empty label.
Page: 7
Section: 2.1

Name: Update label
Definition: A comma separated list of expressions with a side-effect; expressions must only refer to clocks, integer variables, and constants and only assign integer values to clocks. They may also call functions.
Page: 7
Section: 2.1

Name: Invariant
Definition: it is side-effect free
Page: 7
Section: 2.1
Definition2: only clock, integer variables, and constants are referenced
Conjdef: it
Definition3: e evaluates to an integer and x is a clock
DefType: a conjunction of conditions of the form x<e or x<=e

Name: A state formula
Definition: an expression (see Fig. 33) that can be evaluated for a state without looking at the behaviour of the model
Page: 7
Section: 2.2

Instruction: deadlock
Page: 7
Effect: A state formula true in each deadlock state
Section: 2.2

Name: A deadlock state
Definition: A state such that there are no outgoing action transitions neither from the state itself or any of its delay successors
Page: 7
Section: 2.2

Name: A reachability properties
Definition: A property stating that some formula can possibly be satisfied
Page: 7
Section: 2.2

Name: A safety properties
Definition: A property stating that something will never happen
Page: 8
Section: 2.2

Name: An inactive variable
Definition: A variable which is reset before the next time it is read
Page: 27
Section: 7.1

Name: Variable reduction
Definition: Resetting a variable when it becomes inactive.
Page: 27
Section: 7.1

Name: Clock reduction
Definition: Resetting a clock when it becomes inactive.
Page: 28
Section: 7.1