Ignore:
Timestamp:
Oct 19, 2011, 11:30:24 AM (10 years ago)
Author:
sacerdot
Message:
  1. Added joint/BEGlobalenvs that is a modification of common/Globalenvs where
    • the memory used is the back-end one
    • no lookup via values is implemented
    • global variables are never initialized in the back-end
  2. Added to all semantics some default value to initialize the initial state
  3. Initial state initialization (in joint/semantics.ma) almost completed.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/joint_LTL_LIN_semantics.ma

    r1390 r1408  
    66 λsuccT,succ,pointer_of_label.
    77 mk_more_sem_params ?
    8   unit hw_register_env succ
     8  unit it hw_register_env empty_hw_register_env 0 it succ
    99   hwreg_store hwreg_retrieve (λ_.hwreg_store RegisterA) (λe.λ_.hwreg_retrieve e RegisterA)
    1010    (λ_.hwreg_store RegisterB) (λe.λ_.hwreg_retrieve e RegisterB)
Note: See TracChangeset for help on using the changeset viewer.