| #
86bcdc60 |
|
02-May-2019 |
Michael Norrish <Michael.Norrish@nicta.com.au> |
Fix examples/PSL 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
|
| #
bda813d1 |
|
15-Oct-2018 |
Thomas Tuerk <thomas@tuerk-brechen.de> |
rename PSL-Path theory
in "examples/PSL/path" rename
PathTheory -> PSLPathTheory
FinitePathTheory -> FinitePSLPathTheory
this eliminates the clash of theory names with "src/coalgebras/path"
|
| #
365c2060 |
|
18-Sep-2018 |
Chun Tian (binghe) <binghe.lisp@gmail.com> |
Fixed PSL examples (1.01/official-semantics, 1.01/executable-semantics, 1.1/official-semantics)
|
| #
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!
|
| #
5a504130 |
|
04-Mar-2008 |
Peter Homeier <palantir@trustworthytools.com> |
Fixed various proof scripts in ProjectionScript.sml so that examples/PSL/1.1/official-semantics now builds.
|
| #
b538cbda |
|
11-Oct-2004 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Fixing a module open loop (not sure how it arose).
|
| #
6a52fca8 |
|
11-Oct-2004 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Haven't done a checkin for ages, so thought I'd see what would happen
when I did ...
|
| #
47b9a32f |
|
02-Jul-2004 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Moving things around a bit and starting to add more to ModelTheory
needed for project to validate PSL to CTL
(http://www.cl.cam.ac.uk/~mjcg/PSL/psl2ctl/).
|
| #
325af57f |
|
09-Apr-2004 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Just a tweak.
|
| #
aa10ebda |
|
09-Apr-2004 |
Mike Gordon <mjcg@cl.cam.ac.uk> |
Start of a theory validating the projection view (or temporal abstraction).
The aim is to support "cycle-based" evaluation of PSL. So far only a result
for SEREs has been proved.
Define:
|- !l c. LIST_PROJ l c = FILTER (CLOCK c) l
|- !c s. CLOCK c s = B_SEM s c
then:
|- !r l c.
S_CLOCK_FREE r /\ TOP_FREE l /\ BOTTOM_FREE l ==>
((LENGTH l > 0 ==> CLOCK c (LAST l)) /\ US_SEM (LIST_PROJ l c) r
=
S_SEM l c r)
|