Changeset 716 for src/LTL


Ignore:
Timestamp:
Mar 29, 2011, 2:29:12 PM (9 years ago)
Author:
mulligan
Message:

Finished translating LTL statements to LIN statements. Need to implement graph functions.

Location:
src/LTL
Files:
1 added
2 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r714 r716  
    2020  | LTL_St_Op1: Op1 → label → LTLStatement globals
    2121  | LTL_St_Op2: Op2 → Register → label → LTLStatement globals
    22   | LTL_ClearCarry: label → LTLStatement globals
     22  | LTL_St_ClearCarry: label → LTLStatement globals
    2323  | LTL_St_Load: label → LTLStatement globals
    2424  | LTL_St_Store: label → LTLStatement globals
  • src/LTL/LTLToLIN.ma

    r715 r716  
    1717    | LTL_St_Pop lbl ⇒ LIN_St_Pop globals
    1818    | LTL_St_Push lbl ⇒ LIN_St_Push globals
    19 (*    | LTL_St_Address ident proof address lbl ⇒ LIN_St_Address globals ident proof *)
    20     | LTL_St_FromAcc
     19    | LTL_St_Address ident proof address lbl ⇒ LIN_St_Address globals ident proof
     20    | LTL_St_FromAcc register lbl ⇒ LIN_St_FromAcc globals register
     21    | LTL_St_ToAcc register lbl ⇒ LIN_St_ToAcc globals register
     22    | LTL_St_OpAccs opaccs lbl ⇒ LIN_St_OpAccs globals opaccs
     23    | LTL_St_Op1 op1 lbl ⇒ LIN_St_Op1 globals op1
     24    | LTL_St_Op2 op2 register lbl ⇒ LIN_St_Op2 globals op2 register
     25    | LTL_St_ClearCarry lbl ⇒ LIN_St_ClearCarry globals
     26    | LTL_St_Load lbl ⇒ LIN_St_Load globals
     27    | LTL_St_Store lbl ⇒ LIN_St_Store globals
     28    | LTL_St_CallId identifier lbl ⇒ LIN_St_CallId globals identifier
     29    | LTL_St_CondAcc tgt lbl ⇒ LIN_St_CondAcc globals (label_to_Identifier tgt)
     30    | LTL_St_Return ⇒ LIN_St_Return globals
    2131    ].
Note: See TracChangeset for help on using the changeset viewer.