|
Last change
on this file since 1233 was
1233,
checked in by sacerdot, 9 years ago
|
|
1) Ported to Brian's new dependent type for fullexec
2) Universe level raised for fullexec and related stuff to accomodate the
joint semantics
3) Improved joint syntax and semantics
4) Code for LTLToLin simplified
|
|
File size:
471 bytes
|
| Line | |
|---|
| 1 | include "joint/Joint.ma". |
|---|
| 2 | include "common/Graphs.ma". |
|---|
| 3 | |
|---|
| 4 | definition ltl_params: params ≝ |
|---|
| 5 | mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) label. |
|---|
| 6 | |
|---|
| 7 | definition ltl_statement ≝ joint_statement ltl_params. |
|---|
| 8 | |
|---|
| 9 | (*definition ltl_sem_params_: ∀globals. sem_params_ ltl_params globals ≝ |
|---|
| 10 | λglobals. |
|---|
| 11 | mk_sem_params_ ltl_params globals (graph (ltl_statement globals)) (lookup …).*) |
|---|
| 12 | |
|---|
| 13 | definition ltl_program ≝ joint_program ltl_params. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
