-----------------------------------------------------

bin/ptamc examples/pta/simple/iandc.des sr 'z<6'
bin/ptamc examples/pta/simple/tcs.des l3 true
bin/ptamc examples/pta/simple/gethin1.des l2 true
bin/ptamc examples/pta/simple/gethin2.des l2 true
bin/ptamc examples/pta/simple/formats.des l3 true -refine=first -v 

-----------------------------------------------------

More Type checking, semantic checks ???
Make sure checks match Digital clocks, Stochastic games
Time divergence?

Creation of new names (adding extra _s) doesn't take into account prop file ot consts etc.

Sort VarList (two types - before and after constants evaluated). Need for simulator too.


Digital clocks
--------------

Translation done sep for erach property (e.g. for cmax)

Debugging on case studies
Optimisations?
Urgency?


Stochastic games
----------------

Optimise number of states in time-bounded PTAs (extras added in old target states) using until in forwards reach?


* Email Holger/Arndt some models


Documentation
-------------

Where can clocks be used
* clock constraints (just (some) binops)
  - in guards
  - in invariants
* resets (normal updates, but to ints only)
* var decl.s
* generally must be convex (i.e. just conj of constraints) (can be relaxed a bit for digital clocks)

Must have single initial state (is this true for digital clocks too?)