You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
53 lines
1.1 KiB
53 lines
1.1 KiB
Todo
|
|
----
|
|
|
|
* 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
|
|
|
|
|
|
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)
|
|
|
|
Must have single initial state (is this true for digital clocks too?)
|
|
|