#
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
|
#
1760408c |
|
15-Oct-2018 |
Thomas Tuerk <thomas@tuerk-brechen.de> |
rename ltlTheory -> full_ltlTheory In order to avoid a name clash with "examples/logic/ltl/ltl" the theory "examples/temporal_deep/src/deep_embeddings/ltl" was renamed to "full_ltl"
|
#
f51c777e |
|
06-Oct-2018 |
Thomas Tuerk <thomas@tuerk-brechen.de> |
temporal_deep example: ensure it works with both standard and experimental kernel
|
#
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
|