#
3cbdfd88 |
|
20-Apr-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Alter VAR_EQ_TAC to call TIDY_ABBREVS after invocation TIDY_ABBREVS "purges" abbreviations that have become malformed, where - "malformed" means no longer of form Abbrev (var = exp), with exp not itself a variable - "purge" means Abbrev(e1 = e2) becomes e2 = e1, and Abbrev(other_exp) becomes other_exp. The action of TIDY_ABBREVS is included in the ABBREV_ss simpset fragment, which is in turn included in the stateful simpset. The calling of TIDY_ABBREVS is the only change in the behaviour of VAR_EQ_TAC, and this can be turned off with the BasicProvers.var_eq_old trace.
|
#
5ede3b49 |
|
16-Apr-2020 |
Michael Norrish <michael.norrish@data61.csiro.au> |
Fixes for changes to VAR_EQ_TAC etc.
|
#
12e8779a |
|
26-Jul-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix generic_finite_graphs to properly record incoming edges This has some knock-on effects in the examples/logic/ltl directory.
|
#
f251afee |
|
25-Jan-2018 |
Simon Jantsch <simon.jantsch@gmail.com> |
added acceptance sets to gba type
|
#
a061a8d2 |
|
20-Jan-2018 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fixes to build logic/ltl/concrGBArepScript.sml on --expk
|
#
e8b40b28 |
|
18-Jan-2018 |
Simon Jantsch <simon.jantsch@gmail.com> |
finished expgba correct
|
#
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
|
#
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
|
#
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
|
#
ac85e673 |
|
15-Dec-2017 |
Simon Jantsch <simon.jantsch@gmail.com> |
Some progress on showing that the concrete extr_trans functions corresponds to the abstract one
|
#
db9ec12a |
|
10-Dec-2017 |
Simon Jantsch <simon.jantsch@gmail.com> |
addNode Lemma for GBA
|
#
1e37cb3d |
|
09-Dec-2017 |
Simon Jantsch <simon.jantsch@gmail.com> |
Adapted d_conj_concr so all lists will be nubbed Showed how gba_trans_concr relates to d_conj_set
|
#
007e922b |
|
05-Dec-2017 |
Simon Jantsch <simon.jantsch@gmail.com> |
added new concrGBA file and some helpers to generHelpers and concrltl2waa
|