History log of /seL4-l4v-10.1.1/HOL4/examples/logic/ltl/concrwaa2gbaScript.sml
Revision Date Author Comments
# 7cdf00b5 01-Feb-2018 Simon Jantsch <simon.jantsch@gmail.com>

fixed scripts that broke because of renaming a theorem


# d3e6b133 31-Jan-2018 Simon Jantsch <simon.jantsch@gmail.com>

clarify concrete correctness proofs


# 13a31958 29-Jan-2018 Simon Jantsch <simon.jantsch@gmail.com>

make expgba_correct look nicer


# 8d28b9b8 25-Jan-2018 Simon Jantsch <simon.jantsch@gmail.com>

changed wording waa -> vwaa


# f251afee 25-Jan-2018 Simon Jantsch <simon.jantsch@gmail.com>

added acceptance sets to gba type


# 095653b7 19-Jan-2018 Simon Jantsch <simon.jantsch@gmail.com>

fix concr2gba, remove commented code and remove an unused Theory file


# e8b40b28 18-Jan-2018 Simon Jantsch <simon.jantsch@gmail.com>

finished expgba correct


# 4006f532 17-Jan-2018 Michael Norrish <Michael.Norrish@nicta.com.au>

Get logic/ltl/concrwaa2gba to build (commenting out broken stuff)


# 6337c231 16-Jan-2018 Simon Jantsch <simon.jantsch@gmail.com>

started working on FINAL and TRANS


# 5a5d03a0 15-Jan-2018 Simon Jantsch <simon.jantsch@gmail.com>

finished INIT, started on FINAL


# fa52a2ec 14-Jan-2018 Simon Jantsch <simon.jantsch@gmail.com>

finished states for concrwaa2gba, started with init


# 313d62ff 12-Jan-2018 Simon Jantsch <simon.jantsch@gmail.com>

showed some of the preconditions for the STATES goal


# e6499e45 07-Jan-2018 Simon Jantsch <simon.jantsch@gmail.com>

working on correctness of concrete waa2gba


# 9765becb 07-Jan-2018 Simon Jantsch <simon.jantsch@gmail.com>

finished expGBA_reachable


# 9c037895 02-Jan-2018 Simon Jantsch <simon.jantsch@gmail.com>

working on reachable states of concrete gba


# 1dddec08 30-Dec-2017 Simon Jantsch <simon.jantsch@gmail.com>

working on concrete waa2gba function


# c5dca8d3 26-Dec-2017 Simon Jantsch <simon.jantsch@gmail.com>

working on correspondance between concrete and abstract acceptance sets


# c3c5f7f5 24-Dec-2017 Simon Jantsch <simon.jantsch@gmail.com>

working on states for concrete waa2gba


# 42d1fa32 20-Dec-2017 Simon Jantsch <simon.jantsch@gmail.com>

finished termination proof for concr waa2gba


# a8f8bdfd 20-Dec-2017 Simon Jantsch <simon.jantsch@gmail.com>

working on termination of concr waa2gba


# 4e018a7c 20-Dec-2017 Simon Jantsch <simon.jantsch@gmail.com>

working on termination of concrwaa2gba


# 79b532ab 20-Dec-2017 Simon Jantsch <simon.jantsch@gmail.com>

progress on termination of waa2gba


# a5c3f80d 10-Dec-2017 Simon Jantsch <simon.jantsch@gmail.com>

showed the invariants that followers lists in waa are sorted
on the edge group