|
Last change
on this file since 1236 was
1236,
checked in by sacerdot, 9 years ago
|
|
LTLToLin.ma completed (up to a couple of daemons used to provide dead code/data
that will be removed from the joint status later)
|
|
File size:
744 bytes
|
| Rev | Line | |
|---|
| [1168] | 1 | include "joint/Joint.ma". |
|---|
| [491] | 2 | |
|---|
| [1168] | 3 | definition lin_params: params ≝ |
|---|
| [1233] | 4 | mk_params (mk_params_ unit unit unit unit registers_move Register False unit unit unit) unit. |
|---|
| [1168] | 5 | |
|---|
| [1233] | 6 | definition lin_statement ≝ joint_statement lin_params. |
|---|
| [1168] | 7 | |
|---|
| [757] | 8 | definition well_formed_P ≝ |
|---|
| [723] | 9 | λA, B: Type[0]. |
|---|
| 10 | λcode: list (option A × B). |
|---|
| 11 | match code with |
|---|
| 12 | [ nil ⇒ False |
|---|
| 13 | | cons hd tl ⇒ |
|---|
| 14 | match \fst hd with |
|---|
| 15 | [ Some lbl ⇒ False |
|---|
| [1233] | 16 | | None ⇒ True]]. |
|---|
| [1224] | 17 | |
|---|
| [1233] | 18 | (* |
|---|
| [1224] | 19 | definition lin_sem_params_: ∀globals. sem_params_ lin_params globals ≝ |
|---|
| 20 | λglobals. |
|---|
| 21 | mk_sem_params_ lin_params globals (Σcode:list (lin_statement globals). well_formed_P … code) ?. |
|---|
| 22 | (*CSC: lookup function to be implemented *) |
|---|
| 23 | cases daemon |
|---|
| 24 | qed. |
|---|
| [1233] | 25 | *) |
|---|
| [1224] | 26 | |
|---|
| [1236] | 27 | definition lin_program ≝ joint_program lin_params. |
|---|
Note: See
TracBrowser
for help on using the repository browser.
