Title: Theory / Unimportant / CS / Softw / UPPAAL / TIGA
Tags: computer_to_instruction hasNotNewEffectReturnsMeaning FromInstruction fromCommandLine récupéré

Name: A rectangular constraint
Definition: A conjuction of constraints of the form \(x\sim k\) with \(k\in \mathbb Z\), \(x\in C\) and \(\sim\in\{<,\le,=,>,\ge\}\)
Page: 2
Section: 2.1
Variables: \(C\) a set of clock
Denoted by: \(\phi\)

Name: The set of controllable action
Page: 2
Notation: \(\mathrm{Auc}_c\)

Name: The set of uncontrollable action
Page: 2
Notation: \(\mathrm{Auc}_u\)

Fla: -u->
Effect: State that the transition is uncontrollable
Page: 3
Section: 2.2

Name: An implicit transition
Definition: An uncontrollable transition, which is taken because otherwise the invariant would not be satisfied
Page: 3
Section: 2.2

Instruction: A [P W Q]
Page: 6
Effect: Should reach Q and must tay in P
Section: 3.2
Variables: P,Q TCTL formulae
Name: Weak reachability with avoidance

Instruction: A [P U Q]
Page: 5
Effect: Must stay in P until Q holds
Section: 3.2
Variables: P,Q TCTL formulae
Name: Strict reachability with avoidance

Instruction: E[] control:P
Page: 6
Effect: Must satisfy P with the least help from the environment
Section: 3.3
Variables: P TCTL formulae
Name: Partial cooperation

Name: A (controllable) strategy
Definition: A function \(L\times\mathbb R^C_{\ge0}\to \mathrm Act_c\cup\{\lambda\}\)
Page: 6
Section: 3.3
Variables: \(\mathcal A=(L,l_0,C,Act,E,I)\) a Timed Game Automaton

Name: A winning strategy
Definition: A strategy such that the controller supervised by the strategy always win the game whatever actions are chosen by the environmen
Page: 6
Section: 3.3
Variables: \(\mathcal A=(L,l_0,C,Act,E,I)\) a Timed Game Automaton

Instruction: verifytiga foo.xml bar.q
Page: 6
Section: 4.2
Returns: Whether there exists a strategy winning the timed game of foo.xml for the conditions of bar.q

Fla: -t0
Effect: Output a strategy for each given winning condition
Page: 6
Prefix: verifytiga foo.xml bar.q
Section: 4.2

Fla: -c0
Effect: Print one strategy for each discrete state
Page: 6
Prefix: verifytiga foo.xml bar.q
Section: 4.2

Fla: -c1
Effect: Print BCDD strategy for each transition
Page: 6
Prefix: verifytiga foo.xml bar.q
Section: 4.2

Instruction: control_t*(u,g): A[P U Q]
Page: 6
Effect: Must reach Q within less than u-g time units and must stay in P
Section: 4.3
Intuition: Time optimality