%\newcommand{\xrightarrow}[1]{\stackrel{#1}{\rightarrow}} \newcommand{\A}{\mathcal{A}} % a timed automaton \newcommand{\B}{\mathcal{B}} % another one \newcommand{\sem}[1]{\llbracket #1 \rrbracket} \newcommand{\Inv}{{\mathsf{Inv}}} % invariants \newcommand{\Reg}{{\mathsf{Reg}}} % set of regions \newcommand{\Rel}[3]{{\mathsf{Rel}_{#3}(#1,#2)}} % relations between clocks % in the first argument % and clocks in the second % argument \newcommand{\G}[2]{{\mathcal{G}_{#1,(#2)}}} % game (1st argument: TA, % second argument: % ressources) \newcommand{\Act}{{\mathsf{Act}}} % actions in the game \newcommand{\Bad}{{\mathsf{Bad}}} % bad states in the game \newcommand{\V}{{\mathsf{V}}} % vertices in the game \renewcommand{\v}{{\mathsf{v}}} % some vertex \newcommand{\confset}{{\mathcal{E}}} % set of configurations \newcommand{\Succ}{{\mathsf{Succ}}} % successors in the game \newcommand{\up}{{\mathsf{up}}} % update \newcommand{\Aut}[1]{{\mathsf{Aut}(#1)}} % TA associated with a strategy % (in argument) \renewcommand{\L}{\mathcal{L}} % langage (timed words) \newcommand{\traces}{\mathsf{traces}} % traces \definecolor{GrisC}{rgb}{0.86,0.86,0.86}% \newcommand{\cl}{\mathsf{cl}} % (epsilon-)closure \newcommand{\new}[1]{\textcolor{red}{#1}} % nouveau texte \newcommand{\old}[1]{\textcolor{blue}{#1}} % texte a adapter