#
24a59a9e |
|
10-Mar-2020 |
Chun Tian <binghe.lisp@gmail.com> |
`temporal_deep` fixes, selftests and reformats (#792) * Fixed translationsLib due to eqtype changes * Fixes for tight equality * Turned ltl2omega.sml into a selftest * Trying to fix ltl_to_automaton_formulaTheory for tight equality * BUECHO -> BUECHI * Do not run selftest.exe normally * Simplified type definitions using abbreviations * reformated with more comments * reformated * Fixed Holmakefile in examples * Turning modelCheck.sml into a Moscow ML-only selftest * re-formated the entire symbolic_kripke_structureTheory * Added a selftest from modelCheck.sml without using modelCheckLib * More cleanups * More cleanups * stage work commenting symbolic_semi_automatonTheory * Commenting automaton_formulaTheory * Commenting automaton_formulaTheory * Commenting automaton_formulaTheory * Commented automaton_formulaTheory * Commented symbolic_kripke_structureTheory * Reviewed/commented full_ltlTheory * Fixed trailing whitespaces, prepared for submitting * Fixed references * Fixed comments in automaton_formulaTheory * Removed 100+ extra empty lines, done here
|
#
d46b19ab |
|
02-May-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix examples/temporal_deep given tight equality
|
#
18934f7c |
|
03-Dec-2018 |
Johannes Åman Pohjola <johannes.amanpohjola@data61.csiro.au> |
Reconcile store_thms with diverging names in db and val binding
|
#
f51c777e |
|
06-Oct-2018 |
Thomas Tuerk <thomas@tuerk-brechen.de> |
temporal_deep example: ensure it works with both standard and experimental kernel
|
#
81ba0c9a |
|
05-Oct-2018 |
Thomas Tuerk <thomas@tuerk-brechen.de> |
cleanup temporal_deep - replace "ITERATE" with "FUNPOW" - replace "POWER_SET" with "POW" - replace "PRED_SET_FORALL" with "RES_FORALL" - move "POS_START" to translationsLib and plan for later removal - remove various lemmata and use lemmata from standard libs instead - remove Know and Suff
|
#
7d68bd97 |
|
05-Oct-2018 |
Thomas Tuerk <thomas@tuerk-brechen.de> |
work on temporal_deep example Following some work by Chun Tian, this commit makes the temporal_deep example compile again. This example got severe bit-rot unluckily. There is still more work to do: - the libraries have not been tested yet - the theories contaimn now many constants and lemmata now present in standard libraries - the proofs are ugly using strange constructs which are hard to maintain (I hope I learned something about HOL within the last 10 years since I created this example) So, this commit is just a first step and more cleanup work will follow.
|
#
b7e2d444 |
|
17-Sep-2018 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Stage work on fixing temporal_deep example (tools)
|
#
ab4a4cbb |
|
03-Feb-2015 |
Piotr Trojanek <piotr.trojanek@gmail.com> |
remove executable bit from text files in examples/
|
#
4761143b |
|
10-Aug-2009 |
Tjark Weber <Tjark.Weber@cl.cam.ac.uk> |
Removed trailing whitespace from all .sml and .sig files. This affects over 900 files and was done using emacs's delete-trailing-whitespace function in batch mode. Building the system with Poly/ML and Moscow ML seems to work, so I'm hoping these changes don't break anything. Please complain if they do!
|
#
1e90d3ff |
|
18-Oct-2006 |
Thomas Tuerk <Thomas.Tuerk@cl.cam.ac.uk> |
Some deep embeddings of temporal logics and some related tools. Especially there are translations between PSL and LTL and between LTL and omega-automata. Additionally, there is an interface to SMV
|