How to formally describe this Uppaal automata?

249 Views Asked by At

I have the following simple automata:

enter image description here

What I'm looking for is a formal description of this based on the definition here

$A=(\Sigma,\Gamma,S,s_0,\delta,\omega, F)$

How to declare all the variables? Or do I need a different definition for this kind of automata?

What I got is the following, but I'm not sure about most parts of it:

$\Sigma = \{i_{in}\}$
$\Gamma = \{i_{out}\}$ $S = \{Init, Inc, Reset\}$ with $s_0 = Init$.
$\delta$ somehow contains $\Delta = \{(Init, Inc), (Inc, Init), (Init, Reset), (Reset, Init)\} $ and has to be depend on $\Sigma$.

And how is $\omega$ defined?

Please tell me how to do this right, or maybe show me some tutorials that might help. Thanks

1

There are 1 best solutions below

0
On BEST ANSWER

I found the solution in a description of the tool I'm using: Uppaal New Tutorial