TODO (before any release)
-------------------------

* GUI

* Clarify semantic/type checks (consistency with games/digital)

* Clarify time divergence issues

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

* Digital clocks: No time-bounded until yet
* Digital clocks: Translation done sep for each property (e.g. for cmax)?

* BRP example

* Clarify issue of PTAs accessing non-local vars (currently don't allow this because doesn't work with AR approach which converts to PTA objects first). But this rules out message passing.


Bugs
----


Maybe todo
----------

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

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

* Digital clocks: urgency?

* Digital clocks: optimisations?


Tidy
----

* Remove unneeded files from examples (prism-benchmark, rewards stuff)


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)

Currently, modules cannot access non-local vars (and there are no globals)
(this is too restrictive, e.g. for message passing)

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

Invariants must come straight after var decls