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

Question: Which part of C is not accepted in UPPAAL
Answer: Pointers,
Page: http://people.cs.aau.dk/~adavid/utap/syntax.html
Answer2: recursive functions
Answer3: goto
Answer4: bitwidth of fields
Answer5: enumeration/union types
Answer6: comma is limited
Answer7: bitwise negation

Instruction: foo.bar
Page: manual Requirement
Returns: Whether process foo is in location bar

Instruction: p-->q
Page: manual Requirement
Effect: Shorthand for A[] (p imply A<>q)

Instruction: deadlock
Page: manual Requirement
Effect: for all \(d>=0\), there is no action successor of \((L,v+d)\)

Typ: meta foo
Meaning: the type of foo, but not considered when checking for equality of states.
Page: manual Requirement
Name: Meta variable

Name: A location
Definition: A name (optional), to refer to it in requirement, and to document
Page: locations
Chapter: manual
Section: Language reference, >system description> templates
Definition2: Invariant: conjunction of clocks bounded above by an integer, differences between clocks, and Boolean expressions not involving clocks
Conjdef: A structure with
Definition3: Whether it is initial/urgent/committed

Name: An edge
Definition: Selections: non-deterministically bind a given identifier to a value in a given range. The other three labels of an edge are within the scope of this binding.
Page: locations
Chapter: manual
Section: Language reference, >system description> templates
Definition2: Guards: An edge is enabled in a state if and only if the guard evaluates to true.
Conjdef: structure with
Definition3: Synchronisation: Processes can synchronize over channels. Edges labelled with complementary actions over a common channel synchronise.
Definition4: Updates: When executed, the update expression of the edge is evaluated. The side effect of this expression changes the state of the system.

Instruction: foo: bar
Page: locations
Effect: Assign to foo, a new local variable, an arbitrary element of type bar
Context: Edge in Uppaal
Chapter: manual
Section: Language reference, >system description> templates
Intuition: Selections

Name: guard
Definition: simple conditions on clocks,
Page: locations
Chapter: manual
Section: Language reference, >system description> templates
Context: UPPAAL Edge
Definition2: differences between clocks
Definition3: boolean expressions not involving clocks
Extra: The bound must be given by an integer expression.
DefType: a conjunction