diff --git a/benchmarks/basic/ai/basic.c b/benchmarks/basic/ai/basic.c
index 76d4103..3127f42 100644
--- a/benchmarks/basic/ai/basic.c
+++ b/benchmarks/basic/ai/basic.c
@@ -3,23 +3,22 @@
 int x = 0;
 
 void *p(void* arg){
-  x = x + 1;
+  int y = 1;
 }
 
 
 int main(){
   /* references to the threads */
-  pthread_t p_t;
-  pthread_t q_t;
+  pthread_t p_t[2];
   
   /* create the threads and execute */
-  pthread_create(&p_t, NULL, p, NULL);
-  pthread_create(&q_t, NULL, p, NULL);
+  pthread_create(&p_t[0], NULL, p, NULL);
+  pthread_create(&p_t[1], NULL, p, NULL);
   
   /* wait for the threads to finish */
-  pthread_join(&p_t, NULL);
-  pthread_join(&q_t, NULL);
-  
+  pthread_join(&p_t[1], NULL);
+  pthread_join(&p_t[0], NULL);
+ 
   return 0;
 }
 
diff --git a/src/Domain/Action.hs b/src/Domain/Action.hs
index 7fb81ab..dae6590 100644
--- a/src/Domain/Action.hs
+++ b/src/Domain/Action.hs
@@ -9,6 +9,7 @@
 module Domain.Action where
 
 import Language.SimpleC.AST
+import Domain.MemAddr
 import Domain.Util
 import Model.GCS
 
@@ -16,45 +17,48 @@ import Model.GCS
 -- Action using read write sets
 -- over the memory addresses 
 -- accessed.
-data Act
+data Act v
   = Act
-  { rds     :: MemAddrs -- read
-  , wrs     :: MemAddrs -- write
-  , locks   :: MemAddrs -- locks
-  , unlocks :: MemAddrs -- unlocks
-  , tcreate :: MemAddrs -- phtread_create 
-  , tjoin   :: MemAddrs -- phtread_join
-  , texit   :: MemAddrs -- phtread_exit
+  { rds     :: MemAddrs v -- read
+  , wrs     :: MemAddrs v -- write
+  , locks   :: MemAddrs v -- locks
+  , unlocks :: MemAddrs v -- unlocks
+  , tcreate :: MemAddrs v -- phtread_create 
+  , tjoin   :: MemAddrs v -- phtread_join
+  , texit   :: MemAddrs v -- phtread_exit
   }
   deriving (Eq,Ord)
 
-instance Show Act where
+instance Show v => Show (Act v) where
   show (Act r w l u c j e) = 
     "Act { r = " ++ show r ++ ", w = " ++ show w ++ ", lk = " ++ show l ++ ", ulk = " ++ show u ++ ", c = " ++ show c ++ ", j = " ++ show j ++ ", e = " ++ show e
  
-bot_act :: Act
+bot_act :: Act v
 bot_act =
   Act bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs
 
-read_act :: SymId -> Scope -> Act
-read_act sym scope = Act (MemAddrs [MemAddr sym scope]) bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs
+read_act :: SymId -> v -> Scope -> Act v
+read_act sym offset scope = Act (MemAddrs [MemAddr sym offset scope]) bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs
 
-write_act :: SymId -> Scope -> Act
-write_act sym scope = Act bot_maddrs (MemAddrs [MemAddr sym scope]) bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs
+write_act :: SymId -> v -> Scope -> Act v
+write_act sym offset scope = Act bot_maddrs (MemAddrs [MemAddr sym offset scope]) bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs
 
-create_thread_act :: SymId -> Act
-create_thread_act tid = 
-  Act bot_maddrs bot_maddrs bot_maddrs bot_maddrs (MemAddrs [MemAddr tid Global]) bot_maddrs bot_maddrs
+write_act_addr :: MemAddrs v -> Act v
+write_act_addr addr = Act bot_maddrs addr bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs
 
-join_thread_act :: SymId -> Act
-join_thread_act tid = 
-  Act bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs (MemAddrs [MemAddr tid Global]) bot_maddrs 
+create_thread_act :: SymId -> v -> Act v
+create_thread_act tid offset = 
+  Act bot_maddrs bot_maddrs bot_maddrs bot_maddrs (MemAddrs [MemAddr tid offset Global]) bot_maddrs bot_maddrs
 
-exit_thread_act :: SymId -> Act
-exit_thread_act tid = 
-  Act bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs (MemAddrs [MemAddr tid Global]) 
+join_thread_act :: SymId -> v -> Act v
+join_thread_act tid offset = 
+  Act bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs (MemAddrs [MemAddr tid offset Global]) bot_maddrs 
+
+exit_thread_act :: SymId -> v -> Act v
+exit_thread_act tid offset = 
+  Act bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs (MemAddrs [MemAddr tid offset Global]) 
  
-join_act :: Act -> Act -> Act
+join_act :: Eq v => Act v -> Act v -> Act v
 join_act a1 a2 =
   let r = rds a1 `join_maddrs` rds a2 
       w = wrs a1 `join_maddrs` wrs a2 
@@ -65,22 +69,12 @@ join_act a1 a2 =
       e = texit a1 `join_maddrs` texit a2
   in Act r w l u c j e 
 
-add_writes :: MemAddrs -> Act -> Act
+add_writes :: Eq v => MemAddrs v -> Act v -> Act v
 add_writes ws act@Act{..} =
   let wrs' = ws `join_maddrs` wrs
   in act { wrs = wrs' }
   
-{-
-instance Show Act where
-  show act@Act{..} =
-    let rs = "reads: " ++ show rds
-        wrds = "writes: " ++ show wrs
-        lks = "locks: " ++ show locks
-        ulks = "unlocks: " ++ show unlocks
-    in rs++"\n"++wrds++"\n"++lks++"\n"++ulks
--}
-
-instance Action Act where
+instance Eq v => Action (Act v) where
   isBlocking act@Act{..} = 
     not (is_maddrs_bot locks && is_maddrs_bot unlocks)
   isJoin act@Act{..} = 
@@ -111,14 +105,11 @@ instance Action Act where
   isCreateOf tid_sym a1@Act{..} =
     case tcreate of
       MemAddrTop -> True
-      MemAddrs at -> any (\a -> a == MemAddr tid_sym Global) at 
-
-is_global :: MemAddrs -> Bool
-is_global maddr = case maddr of
-  MemAddrTop -> True
-  MemAddrs l -> any (\a@MemAddr{..} -> level == Global) l
+      MemAddrs at -> any (\a -> case a of 
+         MemAddr tid_sym _ Global -> True
+         _ -> False) at 
 
-act_addrs :: Act -> MemAddrs
+act_addrs :: Eq v => Act v -> MemAddrs v
 act_addrs a@Act{..} =
   rds `join_maddrs` wrs `join_maddrs` locks `join_maddrs` 
   unlocks `join_maddrs` tcreate `join_maddrs` tjoin  `join_maddrs` texit
diff --git a/src/Domain/Interval/Collapse.hs b/src/Domain/Interval/Collapse.hs
index a09bbbf..ac22b5c 100644
--- a/src/Domain/Interval/Collapse.hs
+++ b/src/Domain/Interval/Collapse.hs
@@ -1,4 +1,6 @@
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 -------------------------------------------------------------------------------
 -- Module    :  Domain.Interval.Collapse
@@ -16,6 +18,7 @@ import Domain.Action
 import Domain.Interval.Converter
 import Domain.Interval.State
 import Domain.Interval.Value
+import Domain.Interval.API
 import Domain.Util
 import Language.SimpleC.AST
 import Language.SimpleC.Converter (get_symbol_name)
@@ -26,12 +29,12 @@ import qualified Data.Map as M
 import qualified Data.Set as S
 import qualified Debug.Trace as T
 
-type IntGraph = Graph SymId () (IntState,Act) 
-type IntGraphs = Graphs SymId () (IntState,Act)
+type IntGraph = Graph SymId () (IntState,IntAct) 
+type IntGraphs = Graphs SymId () (IntState,IntAct)
 type WItem = (NodeId,EdgeId,NodeId)
 type Worklist = [WItem]
-type ResultList = [(IntState,Pos,Act)]
-type NodeTable = Map NodeId [(IntState,Act)]
+type ResultList = [(IntState,Pos,IntAct)]
+type NodeTable = Map NodeId [(IntState,IntAct)]
 
 data FixState =
   FixState
@@ -52,16 +55,17 @@ showResultList l = "Data Flow Information:\n" ++ (snd $ foldr (\(s,p,a) (n,r) ->
        s_r = s_a ++ show s
    in (n+1, s_r ++ r))  (1,"") l)
 
-is_locked :: System IntState Act -> SExpression -> IntState -> Bool
-is_locked syst expr st = 
-  let lk_ident = get_expr_id expr 
-  in case M.lookup lk_ident (heap st) of
-       Nothing -> error $ "is_locked fatal: cant find info for lock " ++ show lk_ident
-       Just (MCell _ val) -> case val of
-         IntVal [VInt i] -> i == 1  
-         _ -> error $ "is_locked fatal: lock has unsupported values " ++ show val 
+is_locked :: IntState -> Scope -> SExpression -> Bool
+is_locked st scope expr = 
+  let lk_addrs = get_addrs st scope expr 
+  in case read_memory st lk_addrs of
+    []    -> error $ "is_locked fatal: cant find info for lock " ++ show expr
+    [val] -> case val of 
+      IntVal [VInt i] -> i == 1  
+      _ -> error $ "is_locked fatal: lock has unsupported values " ++ show val 
+    l -> error $ "is_locked fatal: lock has unsupported values " ++ show l 
 
-is_live :: TId -> System IntState Act -> EdgeId -> IntGraph -> IntState -> Bool
+is_live :: TId -> System IntState IntAct -> EdgeId -> IntGraph -> IntState -> Bool
 is_live tid syst eId cfg st = 
   let EdgeInfo tags code = get_edge_info cfg eId 
   in case code of
@@ -70,12 +74,13 @@ is_live tid syst eId cfg st =
         "pthread_join" ->
           let tid' = get_tid_expr (Local tid) st (args!!0) 
           in not $ is_enabled syst st tid' 
-        "pthread_mutex_lock" -> not $ is_locked syst (args!!0) st 
+         -- assume the mutex is declared globally 
+        "pthread_mutex_lock" -> not $ is_locked st Global (args!!0)
         _ -> True 
       _ -> True
     _ -> True
  
-instance Collapsible IntState Act where
+instance Collapsible IntState IntAct where
   is_enabled syst st tid =
     let control = controlPart st
         tid_cfg_sym = toThCFGSym st tid
@@ -129,7 +134,7 @@ up_pc i@IntTState{..} t p =
   let st' = update_pc st t p
   in i {st = st'} 
 
-handle_mark :: WItem -> FixOp (IntState,Pos,Act)
+handle_mark :: WItem -> FixOp (IntState,Pos,IntAct)
 handle_mark (pre,eId,post) = do
   fs@FixState{..} <- get
   let node_st = case get_node_info fs_cfg pre of
@@ -157,7 +162,7 @@ handle_mark (pre,eId,post) = do
   case M.lookup post $ node_table cfg' of
     Just [(res_st,res_act)] -> do
       let rwlst = map (\(a,b) -> (post,a,b)) $ succs fs_cfg post
-          e_act = exit_thread_act $ SymId fs_tid
+          e_act = exit_thread_act (SymId fs_tid) zero
       if (Exit `elem` edge_tags) || null rwlst
       then return (res_st,post,res_act `join_act` e_act)
       else return (res_st,post,res_act)
@@ -216,7 +221,7 @@ worklist _wlist = mtrace ("worklist: " ++ show _wlist) $ do
         let nwlist = if is_fix then wlist else (wlist ++ rwlst)
         worklist nwlist
 
-join_update :: NodeTable -> NodeId -> (IntState, Act) -> (Bool, NodeTable)
+join_update :: NodeTable -> NodeId -> (IntState, IntAct) -> (Bool, NodeTable)
 join_update node_table node (st,act) =
   case M.lookup node node_table of
     Nothing -> (False, M.insert node [(st,act)] node_table)
@@ -230,7 +235,7 @@ join_update node_table node (st,act) =
            else (False, M.insert node [(nst,nact)] node_table)
       _ -> error "join_update: more than one state in the list"
  
-strong_update :: NodeTable -> NodeId -> (IntState,Act) -> (Bool, NodeTable)
+strong_update :: NodeTable -> NodeId -> (IntState,IntAct) -> (Bool, NodeTable)
 strong_update node_table node (st,act) =
   case M.lookup node node_table of
     Nothing -> (False, M.insert node [(st,act)] node_table) 
diff --git a/src/Domain/Interval/Converter.hs b/src/Domain/Interval/Converter.hs
index a8de880..2c11a51 100644
--- a/src/Domain/Interval/Converter.hs
+++ b/src/Domain/Interval/Converter.hs
@@ -23,7 +23,9 @@ import qualified Data.Set as S
 import Domain.Interval.State
 import Domain.Interval.Value
 import Domain.Interval.Type
+import Domain.Interval.API
 import Domain.Action
+import Domain.MemAddr
 import Domain.Util
 
 import Language.C.Syntax.Ops 
@@ -43,7 +45,7 @@ data IntTState
    scope :: Scope
  , st :: IntState          -- the state
  , sym :: Map SymId Symbol
- , i_cfgs :: Graphs SymId () (IntState,Act)
+ , i_cfgs :: Graphs SymId () (IntState, IntAct)
  , cond :: Bool            -- is a condition? 
  }
 
@@ -63,7 +65,7 @@ join_state nst = do
 
 -- | converts the front end into a system
 -- @REVISED: July'16
-convert :: FrontEnd () (IntState,Act) -> GCS.System IntState Act
+convert :: FrontEnd () (IntState,IntAct) -> GCS.System IntState IntAct
 convert fe = 
   let (pos_main,sym_main) = get_entry "main" (cfgs fe) (symt fe)
       init_tstate = IntTState Global empty_state (symt fe) (cfgs fe) False
@@ -72,7 +74,7 @@ convert fe =
   in trace ("convert: " ++ show (cfgs fe)) $ GCS.System st' acts (cfgs fe) (symt fe) [GCS.main_tid] 1
 
 -- | retrieves the entry node of the cfg of a function
-get_entry :: String -> Graphs SymId () (IntState, Act) -> Map SymId Symbol -> (GCS.Pos, SymId)
+get_entry :: String -> Graphs SymId () (IntState, IntAct) -> Map SymId Symbol -> (GCS.Pos, SymId)
 get_entry fnname graphs symt = 
   case M.foldrWithKey aux_get_entry Nothing graphs of
     Nothing -> error $ "get_entry: cant get entry for " ++ fnname
@@ -89,15 +91,15 @@ get_entry fnname graphs symt =
                       else Nothing 
 
 -- | processes a list of declarations 
-transformer_decls :: [SDeclaration] -> IntTOp Act
+transformer_decls :: [SDeclaration] -> IntTOp IntAct
 transformer_decls =
   foldM (\a d -> transformer_decl d >>= \a' -> return $ join_act a a') bot_act 
 
 -- | transformer for a declaration:
-transformer_decl :: SDeclaration -> IntTOp Act
+transformer_decl :: SDeclaration -> IntTOp IntAct
 transformer_decl decl = trace ("transformer_decl: " ++ show decl) $ do
   case decl of
-    TypeDecl ty -> error "convert_decl: not supported yet"
+    TypeDecl ty -> error "trannsformer_decl: not supported yet"
     Decl ty el@DeclElem{..} ->
       case declarator of
         Nothing -> 
@@ -118,34 +120,28 @@ transformer_decl decl = trace ("transformer_decl: " ++ show decl) $ do
 --   so any lookup would fail.
 --   This function needs to receive a state and can 
 --   potentially create several states. 
-transformer_init :: SymId -> STy -> Maybe (Initializer SymId ()) -> IntTOp Act
+transformer_init :: SymId -> STy -> Maybe (Initializer SymId ()) -> IntTOp IntAct
 transformer_init id ty minit = trace ("transformer_init for " ++ show id ++ " with init " ++ show minit) $ do
   case minit of
     Nothing -> do
       s@IntTState{..} <- get
       let val = default_value ty
-          st' = case scope of 
-                  Global -> insert_heap st id ty val
-                  Local i -> insert_local st i id val 
-          id_addrs = get_addrs_id st scope id
-          acts = Act bot_maddrs id_addrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs bot_maddrs
+          id_addr = MemAddr id 0 scope
+          st' = write_memory_addr st id_addr val  
+          acts = write_act_addr $ MemAddrs [id_addr]
       set_state st'
       return acts
-    Just i  ->
-      case i of
-        InitExpr expr -> do
-          -- for each state, we need to apply the transformer
-          s@IntTState{..} <- get
-          (val,acts) <- transformer expr
-          let st' = case scope of
-                      Global -> insert_heap st id ty val
-                      Local i -> insert_local st i id val 
-              id_addrs = get_addrs_id st scope id
-              -- this is wrong because id_addrs can be shared among threads
-              acts' = add_writes id_addrs acts
-          set_state st'
-          return acts'
-        InitList list -> error "initializer list is not supported"
+    Just i  -> case i of
+      InitExpr expr -> do
+        -- for each state, we need to apply the transformer
+        s@IntTState{..} <- get
+        (val, acts) <- transformer expr
+        let id_addr = MemAddr id 0 scope
+            st' = write_memory_addr st id_addr val 
+            acts' = add_writes (MemAddrs [id_addr]) acts
+        set_state st'
+        return acts'
+      InitList list -> error "transformer_init: initializer list is not supported"
 
 -- | Default value of a type
 --   If we are given a base type, then we
@@ -164,7 +160,7 @@ default_value ty = --  [ ConVal $ init_value ty ]
 -- | Transformers for interval semantics 
 -- Given an initial state and an expression
 -- return the updated state.
-transformer_expr :: SExpression -> IntTOp Act
+transformer_expr :: SExpression -> IntTOp IntAct
 transformer_expr expr = trace ("transformer_expr: " ++ show expr) $ do
   s@IntTState{..} <- get
   if cond
@@ -177,7 +173,7 @@ transformer_expr expr = trace ("transformer_expr: " ++ show expr) $ do
 -- we are going to be conservative;
 -- all the variables in this expression
 -- are going to be considered written
-bool_transformer_expr :: SExpression -> IntTOp Act
+bool_transformer_expr :: SExpression -> IntTOp IntAct
 bool_transformer_expr expr = trace ("bool_transformer") $ case expr of
   Binary op lhs rhs -> do 
     (val,act) <- apply_logic op lhs rhs
@@ -187,7 +183,7 @@ bool_transformer_expr expr = trace ("bool_transformer") $ case expr of
     in bool_transformer_expr rhs' 
   _ -> error $ "bool_transformer_expr: not supported " ++ show expr
 
-apply_logic :: BinaryOp -> SExpression -> SExpression -> IntTOp (IntValue,Act)
+apply_logic :: BinaryOp -> SExpression -> SExpression -> IntTOp (IntValue,IntAct)
 apply_logic op lhs rhs =
   let one = Const $ IntConst $ CInteger 1 DecRepr $ Flags 0 
   in case op of
@@ -225,7 +221,7 @@ apply_logic op lhs rhs =
 -- Logical Operations
 -- Less than (CLeOp)
 -- Need to update the variables
-interval_leq :: SExpression -> SExpression -> IntTOp (IntValue,Act)
+interval_leq :: SExpression -> SExpression -> IntTOp (IntValue,IntAct)
 {-
 interval_leq (Ident x_i) rhs =
   let v' = lowerBound $ eval rhs s
@@ -254,7 +250,7 @@ interval_leq lhs rhs = do
   return (lhs_val `iMeet` rhs_val, lhs_act `join_act` rhs_act)
 
 -- | Transformer for an expression with a single state
-transformer :: SExpression -> IntTOp (IntValue,Act)
+transformer :: SExpression -> IntTOp (IntValue,IntAct)
 transformer e = trace ("transformer: " ++ show e) $
   case e of 
     AlignofExpr expr -> error "transformer: align_of_expr not supported"  
@@ -281,7 +277,7 @@ transformer e = trace ("transformer: " ++ show e) $
     ComplexImag expr -> error "transformer: complex op not supported" 
 
 -- | Transformer for an assignment expression.
-assign_transformer :: AssignOp -> SExpression -> SExpression -> IntTOp (IntValue,Act)
+assign_transformer :: AssignOp -> SExpression -> SExpression -> IntTOp (IntValue,IntAct)
 assign_transformer op lhs rhs = do
   -- process the lhs (get the new state, values and actions)
   (lhs_vals,lhs_acts) <- transformer lhs
@@ -303,13 +299,13 @@ assign_transformer op lhs rhs = do
       res_acts = add_writes lhs_id (rhs_acts `join_act` lhs_acts)
   -- modify the state of the addresses with
   -- the result values 
-  let res_st = modify_state scope st lhs_id res_vals
+  let res_st = write_memory st lhs_id res_vals
   set_state res_st 
-  return (res_vals,res_acts) 
+  return (res_vals, res_acts) 
 
 -- | Transformer for binary operations.
 --   These transformers do not change the state;
-binop_transformer :: BinaryOp -> SExpression -> SExpression -> IntTOp (IntValue,Act)
+binop_transformer :: BinaryOp -> SExpression -> SExpression -> IntTOp (IntValue,IntAct)
 binop_transformer binOp lhs rhs = do
   s@IntTState{..} <- get
   -- process the lhs (get the new state, values and actions)
@@ -329,7 +325,7 @@ binop_transformer binOp lhs rhs = do
         CXorOp -> error "binop_transformer: CXorOp not supported" 
         CLndOp -> error "binop_transformer: CLndOp not supported" 
         CLorOp -> error "binop_transformer: CLorOp not supported"
-        _ -> error "binop_transtranformer: not completed for intervals" -- apply_logic binOp lhs rhs
+        _ -> error "binop_transtranformer: not completed" -- apply_logic binOp lhs rhs
       res_acts = lhs_acts `join_act` rhs_acts
   return (res_vals,res_acts)
 
@@ -339,7 +335,7 @@ binop_transformer binOp lhs rhs = do
 --   pthread_join
 --   lock
 --   unlock  
-call_transformer :: SExpression -> [SExpression] -> IntTOp (IntValue,Act)
+call_transformer :: SExpression -> [SExpression] -> IntTOp (IntValue,IntAct)
 call_transformer fn args =
   case fn of
     Var ident -> do
@@ -348,7 +344,7 @@ call_transformer fn args =
       call_transformer_name n args 
     _ -> error "call_transformer: not supported" 
 
-call_transformer_name :: String -> [SExpression] -> IntTOp (IntValue,Act)
+call_transformer_name :: String -> [SExpression] -> IntTOp (IntValue,IntAct)
 call_transformer_name name args = case name of
   "pthread_create" -> do
     s@IntTState{..} <- get
@@ -356,22 +352,21 @@ call_transformer_name name args = case name of
         -- pthread_t, the pid of the new thread
     let (tid,s') = inc_num_th st
         th_id = get_addrs s' scope (args !! 0) 
-        s'' = modify_state scope s' th_id (IntVal [VInt tid]) 
+        s'' = write_memory s' th_id (IntVal [VInt tid]) 
         -- retrieve the entry point of the thread code 
         th_sym = get_expr_id $ args !! 2
         th_name = get_symbol_name th_sym sym
         (th_pos,_) = get_entry th_name i_cfgs sym
         --
         i_th_st = bot_th_state th_pos th_sym
-        th_states' = M.insert tid i_th_st (th_states s'')
-        res_st = s'' { th_states = th_states' } 
+        res_st = insert_thread s'' tid i_th_st 
     set_state res_st 
-    return (IntVal [], create_thread_act (SymId tid)) 
+    return (IntVal [], create_thread_act (SymId tid) zero) 
   "pthread_join" -> do
     s@IntTState{..} <- get
     -- this transformer is only called if it is enabled 
     let tid = get_tid_expr scope st (args !! 0)
-    return (IntVal [], join_thread_act (SymId tid)) 
+    return (IntVal [], join_thread_act (SymId tid) zero) 
   "nondet" -> do 
     (lVal,lacts) <- transformer $ args !! 0
     (uVal,uacts) <- transformer $ args !! 1
@@ -386,7 +381,7 @@ call_transformer_name name args = case name of
 -- for the cond + then expression
 -- for the not cond + else expression
 -- and join both states
-cond_transformer :: SExpression -> Maybe SExpression -> SExpression -> IntTOp (IntValue,Act)
+cond_transformer :: SExpression -> Maybe SExpression -> SExpression -> IntTOp (IntValue,IntAct)
 cond_transformer cond mThen else_e = error "cond_transformer not supported"
 {- do
   s <- get
@@ -413,30 +408,30 @@ do
   (vals,acts) <- transformer cond
   -- vals is both false and true 
   let (isTrue,isFalse) = checkBoolVals vals
-  (tVal,tAct) <-
+  (tVal,tIntAct) <-
     if isTrue
     then case mThen of
            Nothing -> error "cond_transformer: cond is true and there is not then"
            Just e -> transformer e
     else return ([],bot_act)
-  (eVal,eAct) <-
+  (eVal,eIntAct) <-
     if isFalse
     then transformer else_e
     else return ([],bot_act)
   let res_vals = tVal ++ eVal
-      res_acts = acts `join_act` tAct `join_act` eAct
+      res_acts = acts `join_act` tIntAct `join_act` eIntAct
   return (res_vals,res_acts) 
 -}
 
 -- | Transformer for constants.
-const_transformer :: Constant -> IntTOp (IntValue,Act)
+const_transformer :: Constant -> IntTOp (IntValue,IntAct)
 const_transformer const =
   case toValue const of
     VInt i -> return (InterVal (I i, I i), bot_act)
     _ -> error "const_transformer: not supported non-int constants"
 
 -- | Transformer for unary operations.
-unop_transformer :: UnaryOp -> SExpression -> IntTOp (IntValue,Act)
+unop_transformer :: UnaryOp -> SExpression -> IntTOp (IntValue,IntAct)
 unop_transformer unOp expr = do 
   case unOp of
     CPreIncOp  -> error "unop_transformer: CPreIncOp  not supported"     
@@ -453,25 +448,13 @@ unop_transformer unOp expr = do
     CNegOp     -> transformer $ negExp expr 
 
 -- | Transformer for var expressions.
-var_transformer :: SymId -> IntTOp (IntValue,Act)
+var_transformer :: SymId -> IntTOp (IntValue, IntAct)
 var_transformer sym_id = do
   s@IntTState{..} <- get
-  -- First search in the heap
-  case M.lookup sym_id (heap st) of
-    Nothing -> 
-      -- If not in the heap, search in the thread
-      case scope of
-        Global -> error "var_transformer: id is not the heap and scope is global"
-        Local i -> case M.lookup i (th_states st) of
-          Nothing -> error "var_transformer: scope does not match the state"
-          Just ths@ThState{..} -> case M.lookup sym_id th_locals of
-            Nothing -> error $ "var_transformer: id " ++ show sym_id ++ " is not in the local state of thread " ++ show th_locals
-            Just v  -> do
-              let reds = read_act sym_id scope 
-              return (v,reds)
-    Just cell@MCell{..} -> do
-      let reds = read_act sym_id Global 
-      return (val,reds)
+  let id_addr = MemAddr sym_id zero scope
+      val = read_memory_addr st id_addr
+      acts = read_act sym_id zero scope
+  return (val, acts)
   
 -- negates logical expression using De Morgan Laws
 negExp :: SExpression -> SExpression
diff --git a/src/Domain/Interval/State.hs b/src/Domain/Interval/State.hs
index ffefd2f..ce855af 100644
--- a/src/Domain/Interval/State.hs
+++ b/src/Domain/Interval/State.hs
@@ -23,9 +23,7 @@ import Model.GCS
 import Util.Generic hiding (safeLookup)
 import qualified Data.IntMap as IM
 import qualified Data.Map as M
-import qualified Debug.Trace as T
 
-mtrace a b = b
 -- | Interval Memory Cell
 type IntMCell = MemCell SymId () IntValue
 
@@ -33,7 +31,22 @@ instance Show IntMCell where
   show (MCell _ val) = show val
 
 -- | Interval Heap
-type IntHeap = Map SymId IntMCell
+type IntHeap = Map IntMAddr IntMCell
+
+-- | A thread state is a control and local data
+type ThStates = Map TId ThState
+type Locals = Map IntMAddr IntValue 
+data ThState =
+  ThState
+  { 
+    th_pos    :: Pos
+  , th_cfg_id :: SymId 
+  , th_locals :: Locals 
+  } 
+  deriving (Show,Eq,Ord)
+
+bot_th_state :: Pos -> SymId -> ThState
+bot_th_state pos cfg_id = ThState pos cfg_id M.empty
 
 -- | The interval domain 
 --   The interval domain is a 
@@ -54,85 +67,27 @@ instance Show IntState where
   show (IntState h s nt b) =
     let h_s = if M.null h 
               then "\t\tEMPTY HEAP\n" ++ h_d
-              else "\t\tHEAP\n" ++ h_d ++ showIntHeap h ++ h_d
+              else "\t\tHEAP\n" ++ h_d ++ showMem h ++ h_d
         s_s = "\t\tTHREADS(" ++ show nt ++ ")\n" ++ h_d ++ showThStates s
         i_s = h_u ++ "\t\tSTATE\n"++ h_d 
     in i_s ++ h_s ++ "\n" ++ s_s ++ h_u 
 
-showIntHeap s = M.foldWithKey (\k m r -> "    " ++ show k ++ " := " ++ show m ++ "\n" ++ r) "" s
-
--- | A thread state is a control and local data
-type ThStates = Map TId ThState
-type Locals = Map SymId IntValue 
-data ThState =
-  ThState
-  { 
-    th_pos    :: Pos
-  , th_cfg_id :: SymId 
-  , th_locals :: Locals 
-  } 
-  deriving (Show,Eq,Ord)
-
--- | get the addresses of an identifier
---   super simple now by assuming not having pointers
-get_addrs_id :: IntState -> Scope -> SymId -> MemAddrs
-get_addrs_id st scope id = 
-  case M.lookup id (heap st) of
-    Nothing -> MemAddrs [MemAddr id scope] 
-    Just i  -> MemAddrs [MemAddr id Global] 
-
--- | get_addrs retrieves the information from the 
---   points to analysis.
---   Simplify to only consider the case where the 
---   the expression is a LHS (var or array index).
-get_addrs :: IntState -> Scope -> SExpression -> MemAddrs
-get_addrs st scope expr = mtrace ("get_addrs: " ++ show expr) $
-  case expr of
-    Var id -> get_addrs_id st scope id 
-    Unary CAdrOp e -> get_addrs st scope e 
-    _ -> error $ "get_addrs: not supported expr " ++ show expr
-
-get_tid_expr :: Scope -> IntState -> SExpression -> TId
-get_tid_expr scope st expr = mtrace ("get_tid_expr: " ++ show expr) $
-  -- get the address(es) referenced by expr
-  let th_addrs = get_addrs st scope expr 
-  in case read_memaddrs st th_addrs of
-    [] -> error $ "get_tid: couldnt find thread for expr " ++ show expr 
-    [v] -> case v of
-      IntVal [VInt tid] -> tid
-      _ -> error $ "get_tid: unexpected intvalue " ++ show v 
-    r -> error $ "get_tid: found too many threads for expr " ++ show expr ++ " " ++ show r 
+showMem s = M.foldWithKey (\k m r -> "    " ++ show k ++ " := " ++ show m ++ "\n" ++ r) "" s
 
 showThStates s = 
   M.foldWithKey (\k t r -> "   Thread: PID = " ++ show k ++ showThState t ++ r) "" s
-
-showThState (ThState p c s) = 
-  let p_s = ", LOC = " ++ show p
-      c_s = ", CFG ID = " ++ show c
-      l_s = "\n" ++ showIntHeap s
-  in p_s ++ c_s ++ l_s ++ "\n" ++ h_d 
-
+ where 
+   showThState (ThState p c s) = 
+     let p_s = ", LOC = " ++ show p
+         c_s = ", CFG ID = " ++ show c
+         l_s = "\n" ++ showMem s
+     in p_s ++ c_s ++ l_s ++ "\n" ++ h_d 
+
+-- | Domain operations
 -- | Initial state which is not bottom
 empty_state :: IntState 
 empty_state = IntState M.empty M.empty 1 False 
 
--- | Set the position in the cfg of a thread
-update_pc :: IntState -> TId -> Pos -> IntState
-update_pc i@IntState{..} tid pos = 
-  let th_st = M.update (\(ThState _ c l) -> Just $ ThState pos c l) tid th_states
-  in i { th_states = th_st }
-
--- | Set the position in the cfg of a thread
---   This can also initialize the state of a thread
-set_pos :: IntState -> TId -> SymId -> Pos -> IntState 
-set_pos st@IntState{..} tid cfg_sym npos = 
-  let th_st' =
-        case M.lookup tid th_states of
-          Nothing -> ThState npos cfg_sym M.empty 
-          Just t@ThState{..} -> t { th_pos = npos }
-      th_states' = M.insert tid th_st' th_states 
-  in st { th_states = th_states' }
-
 -- | Checks for state subsumption
 -- 1. Check bottoms 
 -- 2. Check if the number of threads
@@ -167,7 +122,7 @@ subsumes_interval st1 st2 =
        in if th_pos th1 == th_pos th2
           then M.foldrWithKey' (\sym v b -> check_locals sym v lcs1 && b) True (th_locals th2) 
           else False
-   check_locals :: SymId -> IntValue -> Map SymId IntValue -> Bool 
+   check_locals :: IntMAddr -> IntValue -> Locals -> Bool 
    check_locals sym val2 lcs1 =
      case M.lookup sym lcs1 of
        Nothing -> False
@@ -182,14 +137,7 @@ subsumes_interval st1 st2 =
              val2 = val cell2
          in r && val2 <= val1
  
-instance Projection IntState where
-  controlPart st@IntState{..} = M.map th_pos th_states
-  subsumes a b = subsumes_interval a b
-  isBottom = is_bot 
-  toThCFGSym st@IntState{..} tid = case M.lookup tid th_states of
-    Nothing -> error $ "toThCFGSym: invalid tid " ++ show tid
-    Just t@ThState{..} -> th_cfg_id 
-  
+-- | Join operation
 join_intstate :: IntState -> IntState -> IntState
 join_intstate s1 s2 = case (is_bot s1, is_bot s2) of
   (True,_) -> s2
@@ -227,86 +175,17 @@ join_intmcell m1 m2 =
       _val = (val m1) `iJoin` (val m2)
   in MCell _ty _val
 
--- | API for modifying the state
--- | insert_heap: inserts an element to the heap
-insert_heap :: IntState -> SymId -> STy -> IntValue -> IntState
-insert_heap st@IntState{..} id ty val =
-  let cell = MCell ty val 
-      heap' = M.insert id cell heap
-  in st {heap = heap'}  
-
-modify_heap :: IntState -> SymId -> IntValue -> IntState
-modify_heap st@IntState{..} id val = 
-  let heap' = M.update (update_conmcell val) id heap
-  in st {heap = heap'}
-
-update_conmcell :: IntValue -> IntMCell -> Maybe IntMCell
-update_conmcell nval c@MCell{..} = Just $ c { val = nval } 
-
--- | insert_local: inserts an element to local state 
-insert_local :: IntState -> TId -> SymId -> IntValue -> IntState
-insert_local st@IntState{..} tid sym val = 
- case M.lookup tid th_states of
-    Nothing -> error "insert_local: tid not found in th_states"
-    Just s@ThState{..} ->
-      let locals' = M.insert sym val th_locals
-          s' = s { th_locals = locals' }
-          th_states' = M.insert tid s' th_states
-      in st { th_states = th_states' }
-
--- | modify the state: receives a MemAddrs and a
---   IntValue and assigns the IntValue to the MemAddrs
-modify_state :: Scope -> IntState -> MemAddrs -> IntValue -> IntState
-modify_state scope st addrs vals =
-  case addrs of
-    MemAddrTop -> error "modify_state: top addrs, need to traverse everything"
-    MemAddrs l -> foldr (\a s -> modify_state' scope s a vals) st l
- where
-   modify_state' :: Scope -> IntState -> MemAddr -> IntValue -> IntState
-   modify_state' scope st@IntState{..} add@MemAddr{..} conval =
-     -- First search in the heap 
-     case M.lookup base heap of
-       Nothing ->
-         -- If not in the heap, search in the thread
-         case scope of
-           Global -> error "modify_state: id is not the heap and scope is global"
-           Local i -> insert_local st i base conval 
-       Just _ -> modify_heap st base conval  
-
--- @TODO: Return a list of a just a intvalue by doing a join over all results?
-read_memaddrs :: IntState -> MemAddrs -> [IntValue]
-read_memaddrs st addrs = mtrace ("read_memaddrs: " ++ show addrs) $  
-  case addrs of 
-    MemAddrTop -> error "read_memaddrs: have not implemented MemAddrTop"
-    MemAddrs l -> map (read_memaddr st) l
-
-read_memaddr :: IntState -> MemAddr -> IntValue
-read_memaddr st addr = mtrace ("read_memaddr " ++ show addr) $
-  case level addr of
-    Global -> case M.lookup (base addr) (heap st) of 
-      Nothing   -> error $ "read_memaddr: " ++ show addr 
-      Just cell -> val cell
-    Local tid -> case M.lookup tid (th_states st) of   
-      Nothing -> error $ "read_memaddr: tid " ++ show tid ++ " not found with addr " ++ show addr
-      Just th -> case M.lookup (base addr) (th_locals th) of
-        Nothing -> error $ "read_memaddr: " ++ show addr
-        Just value -> value 
+-- | Projection instance
+instance Projection IntState where
+  controlPart st@IntState{..} = M.map th_pos th_states
+  subsumes a b = subsumes_interval a b
+  isBottom = is_bot 
+  toThCFGSym st@IntState{..} tid = 
+    case M.lookup tid th_states of
+      Nothing -> error $ "toThCFGSym: invalid tid " ++ show tid
+      Just t@ThState{..} -> th_cfg_id 
  
-bot_th_state :: Pos -> SymId -> ThState
-bot_th_state pos cfg_id = ThState pos cfg_id M.empty
-
-inc_num_th :: IntState -> (Int, IntState)
-inc_num_th s@IntState{..} =
-  let n = num_th + 1
-  in (n,s { num_th = n })
-
-insert_thread :: IntState -> SymId -> SymId -> Pos -> IntState 
-insert_thread s sym cfg_sym pos =
-  let (tid,s'@IntState{..}) = inc_num_th s
-      th = bot_th_state pos cfg_sym
-      th_states' = M.insert tid th th_states
-  in s' { th_states = th_states' }
-
+-- | Hashable instances 
 instance Hashable IntState where
   hash s@IntState{..} = hash (heap,th_states,num_th,is_bot) 
   hashWithSalt s st@IntState{..} = hashWithSalt s (heap,th_states,num_th,is_bot) 
@@ -330,12 +209,4 @@ instance Hashable Locals where
 instance Hashable IntMCell where
   hash m@MCell{..} = hash val
   hashWithSalt s m@MCell{..} = hashWithSalt s val
- 
-{-
--- State equality: because I'm using a hashtable I need to stay within the ST monad
-isEqual :: IntState s -> IntState s -> ST s Bool
-isEqual s1 s2 = do
-  l1 <- H.toList s1
-  l2 <- H.toList s2
-  return $ isEqual' l1 l2  
--}
+
diff --git a/src/Domain/Interval/Value.hs b/src/Domain/Interval/Value.hs
index 1ec702d..aa0a9af 100644
--- a/src/Domain/Interval/Value.hs
+++ b/src/Domain/Interval/Value.hs
@@ -12,26 +12,37 @@ module Domain.Interval.Value where
 
 import Data.Hashable
 import Data.List
+import Domain.Interval.Type
+import Domain.Util
+import Domain.Action
+import Domain.MemAddr
+import Language.SimpleC.Util
 import Util.Generic hiding (safeLookup)
 import qualified Data.Set as S
 
-import Language.SimpleC.Util
-import Domain.Util
-import Domain.Interval.Type
+-- | Interval Action
+type IntAct = Act IntValue
+
+-- | Interval Memory Addr
+type IntMAddr = MemAddr IntValue
+type IntMAddrs = MemAddrs IntValue
 
 -- | Value for the interval semantics
 data IntValue
   = IntTop              -- Top value 
   | IntBot              -- Bot value
   | IntVal [Value]      -- Intcrete list of values
-  | InterVal (InterVal,InterVal)  
+  | InterVal (InterVal, InterVal)  
   -- Memory address value: set of addresses
-  | IntMemAddr MemAddrs 
+  | IntMemAddr IntMAddrs 
   -- Array value
   -- Memory address for the positions and the size
   | IntArr [IntValue] Int Bool -- IsTop 
   deriving (Show,Eq)
 
+zero :: IntValue
+zero = IntVal [VInt 0]
+
 instance Ord IntValue where
   (<=) (IntVal i) (IntVal j) = (S.fromList i) `S.isSubsetOf` (S.fromList j)
   (<=) (InterVal (a,b)) (InterVal (c,d)) = a >= c && b <= d
diff --git a/src/Domain/Util.hs b/src/Domain/Util.hs
index 7860abb..ba95686 100644
--- a/src/Domain/Util.hs
+++ b/src/Domain/Util.hs
@@ -11,11 +11,10 @@
 module Domain.Util where
 
 import Data.Hashable
-import Data.List
 import Model.GCS
 import Language.SimpleC.AST
 import Language.SimpleC.Util
-
+ 
 -- | Scope (of a transformer)
 --   It can either be global (if we processing
 --   for example global declarations and so we need
@@ -25,63 +24,6 @@ import Language.SimpleC.Util
 data Scope = Global | Local TId
   deriving (Show,Eq,Ord)
 
--- | Concrete Memory address contains of a base + offset
--- data MemAddr
---   = MemAddr 
---   { base :: ConValue
---   , offset :: ConValue
---   }
---   deriving (Show,Eq,Ord)
--- Simplification
--- @Add Scope to MemAddr!
-data MemAddr
-  = MemAddr 
-  { base :: SymId
-  , level :: Scope }
-  deriving (Show,Eq,Ord)
-
-data MemAddrs
-  = MemAddrTop
-  | MemAddrs [MemAddr]
-  deriving (Eq)
-
-instance Show MemAddrs where
-  show a = case a of
-    MemAddrTop -> "MemAddrTop"
-    MemAddrs l -> show l
-
-instance Ord MemAddrs where
-  m1 <= m2 = case (m1,m2) of 
-    (_,MemAddrTop) -> True
-    (MemAddrTop,MemAddrs l) -> False 
-    (MemAddrs l1,MemAddrs l2) ->
-      all (\a -> a `elem` l2) l1 
-
-bot_maddrs :: MemAddrs
-bot_maddrs = MemAddrs []
-
-is_maddrs_bot :: MemAddrs -> Bool
-is_maddrs_bot maddr =
-  case maddr of
-    MemAddrTop -> False
-    MemAddrs l -> null l
-  
-meet_maddrs :: MemAddrs -> MemAddrs -> MemAddrs
-meet_maddrs a1 a2 =
-  case (a1,a2) of
-    (MemAddrTop,_) -> a2
-    (_,MemAddrTop) -> a1
-    (MemAddrs l1, MemAddrs l2) -> 
-      MemAddrs (l1 `intersect` l2)
-
-join_maddrs :: MemAddrs -> MemAddrs -> MemAddrs
-join_maddrs a1 a2 =
-  case (a1,a2) of
-    (MemAddrTop,_) -> a1
-    (_,MemAddrTop) -> a2
-    (MemAddrs l1, MemAddrs l2) ->
-      MemAddrs (nub $ l1 ++ l2)
- 
 instance Hashable SymId where
   hash (SymId i) = hash i
   hashWithSalt s (SymId i) = hashWithSalt s i
@@ -106,23 +48,3 @@ instance Hashable Value where
     VChar   i -> hashWithSalt s i 
     VString i -> hashWithSalt s i 
 
-instance Hashable MemAddrs where
-  hash m = case m of
-    MemAddrTop -> hash (0::Int)
-    MemAddrs l -> hash l
-  hashWithSalt s m = case m of
-    MemAddrTop -> hashWithSalt s (0::Int)
-    MemAddrs l -> hashWithSalt s l
-
-instance Hashable MemAddr where
-  hash m@MemAddr{..} = hash base
-  hashWithSalt s m@MemAddr{..} = hashWithSalt s base
-
-{- 
--- State equality: because I'm using a hashtable I need to stay within the ST monad
-isEqual :: Sigma s -> Sigma s -> ST s Bool
-isEqual s1 s2 = do
-  l1 <- H.toList s1
-  l2 <- H.toList s2
-  return $ isEqual' l1 l2  
--}
diff --git a/src/Main.hs b/src/Main.hs
index 62244c3..580d9c5 100644
--- a/src/Main.hs
+++ b/src/Main.hs
@@ -17,8 +17,8 @@ import Model.GCS
 --import Unfolderful
 import Control.Monad.ST
 import Domain.Action
-import Domain.Concrete
-import Domain.Concrete.State
+-- import Domain.Concrete
+-- import Domain.Concrete.State
 import Domain.Interval.Collapse
 import Domain.Interval
 import Exploration.UNF.Unfolder  
@@ -34,7 +34,7 @@ import Util.CmdOpts
 import Util.Generic
 -- import Util.Printer
 import qualified Data.Map as M
-import qualified Domain.Concrete.Converter as CC
+-- import qualified Domain.Concrete.Converter as CC
 import qualified Domain.Interval.Converter as IC
 import qualified Exploration.UNF.API as US
 import qualified Exploration.UNF.State as US
@@ -108,16 +108,16 @@ interpret f dom = do
 explore :: FilePath -> Domain -> Bool -> Bool -> IO ()
 explore f dom stl cut = do
   case dom of
-    Concrete -> do
-      fe <- extract "" f
-      let syst = CC.convert fe 
-      ust <- unfolder stl cut syst
-      let (cntr, stats) = (US.cntr ust, US.stats ust)
-      -- putStrLn $ show syst 
-      putStrLn $ show (cntr, stats)
+--    Concrete -> do
+--      fe <- extract "" f
+--      let syst = CC.convert fe 
+--      ust <- unfolder stl cut syst
+--      let (cntr, stats) = (US.cntr ust, US.stats ust)
+--      -- putStrLn $ show syst 
+--      putStrLn $ show (cntr, stats)
 --      (_,_,_,dots) <- unfToDot ust 
 --      writeFile (replaceExtension f ".dot") dots
-      putStrLn "explore end"
+--      putStrLn "explore end"
     Interval -> do 
       fe <- extract "" f
       let syst = IC.convert fe
diff --git a/src/tags b/src/tags
index de0cd22..b11720a 100644
--- a/src/tags
+++ b/src/tags
@@ -1,24 +1,10 @@
-Act	./Domain/Action.hs	19;"	t
-Act	./Domain/Action.hs	20;"	d
+Act	./Domain/Action.hs	20;"	t
+Act	./Domain/Action.hs	21;"	d
 Action	./Model/GCS.hs	96;"	t
 Ai	./Util/CmdOpts.hs	68;"	d
 Alternative	./Exploration/UNF/State.hs	62;"	t
 Alternatives	./Exploration/UNF/State.hs	63;"	t
-CState	./Domain/Concrete/State.hs	52;"	d
-CState	./Domain/Concrete/State.hs	52;"	t
 Collapsible	./Model/GCS.hs	77;"	t
-ConArr	./Domain/Concrete/State.hs	36;"	d
-ConGraph	./Domain/Concrete/Collapse.hs	28;"	t
-ConGraphs	./Domain/Concrete/Collapse.hs	29;"	t
-ConHeap	./Domain/Concrete/State.hs	46;"	t
-ConMCell	./Domain/Concrete/State.hs	40;"	t
-ConMemAddr	./Domain/Concrete/State.hs	33;"	d
-ConTOp	./Domain/Concrete/Converter.hs	49;"	t
-ConTState	./Domain/Concrete/Converter.hs	37;"	t
-ConTState	./Domain/Concrete/Converter.hs	38;"	d
-ConVal	./Domain/Concrete/State.hs	31;"	d
-ConValue	./Domain/Concrete/State.hs	30;"	t
-ConValues	./Domain/Concrete/State.hs	27;"	t
 Concrete	./Util/CmdOpts.hs	54;"	d
 Conf	./Exploration/UNF/State.hs	46;"	d
 Configuration	./Exploration/UNF/State.hs	45;"	t
@@ -35,55 +21,54 @@ Events	./Exploration/UNF/State.hs	42;"	t
 EventsID	./Exploration/UNF/State.hs	21;"	t
 Execute	./Util/CmdOpts.hs	62;"	d
 Explore	./Util/CmdOpts.hs	64;"	d
-FixOp	./Domain/Interval/Collapse.hs	47;"	t
-FixState	./Domain/Interval/Collapse.hs	36;"	t
-FixState	./Domain/Interval/Collapse.hs	37;"	d
+FixOp	./Domain/Interval/Collapse.hs	50;"	t
+FixState	./Domain/Interval/Collapse.hs	39;"	t
+FixState	./Domain/Interval/Collapse.hs	40;"	d
 Frontend	./Util/CmdOpts.hs	61;"	d
 Frontier	./Model/GCS.hs	50;"	t
-Global	./Domain/Util.hs	25;"	d
+Global	./Domain/Util.hs	24;"	d
 HashTable	./Util/Generic.hs	19;"	t
 Histories	./Exploration/UNF/State.hs	58;"	t
 History	./Exploration/UNF/State.hs	57;"	t
 I	./Domain/Interval/Type.hs	15;"	d
-IntArr	./Domain/Interval/Value.hs	32;"	d
-IntBot	./Domain/Interval/Value.hs	25;"	d
-IntGraph	./Domain/Interval/Collapse.hs	29;"	t
-IntGraphs	./Domain/Interval/Collapse.hs	30;"	t
-IntHeap	./Domain/Interval/State.hs	36;"	t
-IntMCell	./Domain/Interval/State.hs	30;"	t
-IntMemAddr	./Domain/Interval/Value.hs	29;"	d
-IntState	./Domain/Interval/State.hs	41;"	t
-IntState	./Domain/Interval/State.hs	42;"	d
-IntTOp	./Domain/Interval/Converter.hs	51;"	t
-IntTState	./Domain/Interval/Converter.hs	40;"	t
-IntTState	./Domain/Interval/Converter.hs	41;"	d
-IntTop	./Domain/Interval/Value.hs	24;"	d
-IntVal	./Domain/Interval/Value.hs	26;"	d
-IntValue	./Domain/Interval/Value.hs	23;"	t
+IntAct	./Domain/Interval/Value.hs	24;"	t
+IntArr	./Domain/Interval/Value.hs	40;"	d
+IntBot	./Domain/Interval/Value.hs	33;"	d
+IntGraph	./Domain/Interval/Collapse.hs	32;"	t
+IntGraphs	./Domain/Interval/Collapse.hs	33;"	t
+IntHeap	./Domain/Interval/State.hs	34;"	t
+IntMAddr	./Domain/Interval/Value.hs	27;"	t
+IntMAddrs	./Domain/Interval/Value.hs	28;"	t
+IntMCell	./Domain/Interval/State.hs	28;"	t
+IntMemAddr	./Domain/Interval/Value.hs	37;"	d
+IntState	./Domain/Interval/State.hs	54;"	t
+IntState	./Domain/Interval/State.hs	55;"	d
+IntTOp	./Domain/Interval/Converter.hs	53;"	t
+IntTState	./Domain/Interval/Converter.hs	42;"	t
+IntTState	./Domain/Interval/Converter.hs	43;"	d
+IntTop	./Domain/Interval/Value.hs	32;"	d
+IntVal	./Domain/Interval/Value.hs	34;"	d
+IntValue	./Domain/Interval/Value.hs	31;"	t
 InterVal	./Domain/Interval/Type.hs	15;"	t
-InterVal	./Domain/Interval/Value.hs	27;"	d
+InterVal	./Domain/Interval/Value.hs	35;"	d
 Interpret	./Util/CmdOpts.hs	63;"	d
 Interval	./Util/CmdOpts.hs	54;"	d
-Local	./Domain/Util.hs	25;"	d
-Locals	./Domain/Concrete/State.hs	70;"	t
-Locals	./Domain/Interval/State.hs	66;"	t
-MemAddr	./Domain/Util.hs	37;"	t
-MemAddr	./Domain/Util.hs	38;"	d
-MemAddrTop	./Domain/Util.hs	44;"	d
-MemAddrs	./Domain/Util.hs	43;"	t
-MemAddrs	./Domain/Util.hs	45;"	d
+Local	./Domain/Util.hs	24;"	d
+Locals	./Domain/Interval/State.hs	38;"	t
+MemAddr	./Domain/MemAddr.hs	21;"	t
+MemAddr	./Domain/MemAddr.hs	22;"	d
+MemAddrTop	./Domain/MemAddr.hs	31;"	d
+MemAddrs	./Domain/MemAddr.hs	30;"	t
+MemAddrs	./Domain/MemAddr.hs	32;"	d
 MinusInf	./Domain/Interval/Type.hs	15;"	d
-NodeTable	./Domain/Interval/Collapse.hs	34;"	t
+NodeTable	./Domain/Interval/Collapse.hs	37;"	t
 Option	./Util/CmdOpts.hs	60;"	t
 PlusInf	./Domain/Interval/Type.hs	15;"	d
 Pos	./Model/GCS.hs	52;"	t
 Prime	./Util/CmdOpts.hs	65;"	d
 Projection	./Model/GCS.hs	70;"	t
-ResultList	./Domain/Concrete/Collapse.hs	31;"	t
-ResultList	./Domain/Interval/Collapse.hs	33;"	t
-Scope	./Domain/Util.hs	25;"	t
-Sigma	./Domain/Concrete/State.hs	58;"	t
-Sigma	./Domain/Concrete/State.hs	59;"	d
+ResultList	./Domain/Interval/Collapse.hs	36;"	t
+Scope	./Domain/Util.hs	24;"	t
 States	./Exploration/UNF/State.hs	68;"	t
 Stid	./Util/CmdOpts.hs	66;"	d
 SymAddr	./Model/GCS.hs	55;"	t
@@ -91,12 +76,9 @@ System	./Model/GCS.hs	36;"	t
 System	./Model/GCS.hs	37;"	d
 TId	./Model/GCS.hs	54;"	t
 Test	./Util/CmdOpts.hs	69;"	d
-ThState	./Domain/Concrete/State.hs	71;"	t
-ThState	./Domain/Concrete/State.hs	72;"	d
-ThState	./Domain/Interval/State.hs	67;"	t
-ThState	./Domain/Interval/State.hs	68;"	d
-ThStates	./Domain/Concrete/State.hs	69;"	t
-ThStates	./Domain/Interval/State.hs	65;"	t
+ThState	./Domain/Interval/State.hs	39;"	t
+ThState	./Domain/Interval/State.hs	40;"	d
+ThStates	./Domain/Interval/State.hs	37;"	t
 UnfOpts	./Exploration/UNF/State.hs	72;"	d
 UnfStats	./Exploration/UNF/State.hs	81;"	d
 UnfolderOp	./Exploration/UNF/State.hs	106;"	t
@@ -105,9 +87,8 @@ UnfolderState	./Exploration/UNF/State.hs	92;"	t
 UnfolderState	./Exploration/UNF/State.hs	93;"	d
 UnfolderStats	./Exploration/UNF/State.hs	80;"	t
 Var	./Util/Generic.hs	18;"	t
-WItem	./Domain/Interval/Collapse.hs	31;"	t
-Worklist	./Domain/Concrete/Collapse.hs	30;"	t
-Worklist	./Domain/Interval/Collapse.hs	32;"	t
+WItem	./Domain/Interval/Collapse.hs	34;"	t
+Worklist	./Domain/Interval/Collapse.hs	35;"	t
 _help	./Util/CmdOpts.hs	19;"	v
 _helpAi	./Util/CmdOpts.hs	52;"	v
 _helpDebug	./Util/CmdOpts.hs	47;"	v
@@ -120,64 +101,48 @@ _helpTest	./Util/CmdOpts.hs	50;"	v
 _program	./Util/CmdOpts.hs	14;"	v
 _summary	./Util/CmdOpts.hs	15;"	v
 absIVal	./Domain/Interval/Type.hs	71;"	v
-act_addrs	./Domain/Action.hs	120;"	v
+act_addrs	./Domain/Action.hs	113;"	v
 acts	./Exploration/UNF/State.hs	31;"	v
-add	./Domain/Concrete/Converter.hs	428;"	v
 add_alte	./Exploration/UNF/API.hs	173;"	v
-add_conval	./Domain/Concrete/State.hs	278;"	v
 add_disa	./Exploration/UNF/API.hs	156;"	v
-add_event	./Exploration/UNF/Unfolder.hs	455;"	v	file:
+add_event	./Exploration/UNF/Unfolder.hs	461;"	v	file:
 add_icnf	./Exploration/UNF/API.hs	138;"	v
-add_mark	./Domain/Interval/Collapse.hs	115;"	v
+add_mark	./Domain/Interval/Collapse.hs	120;"	v
 add_succ	./Exploration/UNF/API.hs	119;"	v
-add_writes	./Domain/Action.hs	69;"	v
+add_writes	./Domain/Action.hs	73;"	v
 ai	Main.hs	197;"	v
 ai_mode	./Util/CmdOpts.hs	122;"	v
 allM	./Util/Generic.hs	22;"	v
-alt2	./Exploration/UNF/Unfolder.hs	650;"	v	file:
+alt2	./Exploration/UNF/Unfolder.hs	656;"	v	file:
 alte	./Exploration/UNF/State.hs	36;"	v
-apply_logic	./Domain/Interval/Converter.hs	191;"	v
-assign_transformer	./Domain/Concrete/Converter.hs	248;"	v
-assign_transformer	./Domain/Interval/Converter.hs	285;"	v
-base	./Domain/Util.hs	39;"	v
-binop_transformer	./Domain/Concrete/Converter.hs	276;"	v
-binop_transformer	./Domain/Interval/Converter.hs	313;"	v
-bool_transformer_expr	./Domain/Interval/Converter.hs	181;"	v
+apply_logic	./Domain/Interval/Converter.hs	187;"	v
+assign_transformer	./Domain/Interval/Converter.hs	281;"	v
+base	./Domain/MemAddr.hs	23;"	v
+binop_transformer	./Domain/Interval/Converter.hs	309;"	v
+bool_transformer_expr	./Domain/Interval/Converter.hs	177;"	v
 botEID	./Exploration/UNF/API.hs	21;"	v
 botEvent	./Exploration/UNF/API.hs	29;"	v
 botID	./Model/GCS.hs	63;"	v
 botName	./Exploration/UNF/API.hs	25;"	v
-bot_act	./Domain/Action.hs	36;"	v
+bot_act	./Domain/Action.hs	37;"	v
 bot_explore	./Exploration/UNF/Unfolder.hs	35;"	v	file:
-bot_maddrs	./Domain/Util.hs	61;"	v
-bot_sigma	./Domain/Concrete/State.hs	84;"	v
-bot_state	./Domain/Concrete/State.hs	87;"	v
-bot_th_state	./Domain/Concrete/State.hs	81;"	v
-bot_th_state	./Domain/Interval/State.hs	296;"	v
-call_transformer	./Domain/Concrete/Converter.hs	313;"	v
-call_transformer	./Domain/Interval/Converter.hs	343;"	v
-call_transformer_name	./Domain/Concrete/Converter.hs	322;"	v
-call_transformer_name	./Domain/Interval/Converter.hs	352;"	v
+bot_maddrs	./Domain/MemAddr.hs	50;"	v
+bot_th_state	./Domain/Interval/State.hs	49;"	v
+call_transformer	./Domain/Interval/Converter.hs	339;"	v
+call_transformer_name	./Domain/Interval/Converter.hs	348;"	v
 catMaybes	./Util/Generic.hs	55;"	v
 cfevs	./Exploration/UNF/State.hs	51;"	v
 cfgs	./Model/GCS.hs	42;"	v
-cfgst	./Domain/Concrete/Converter.hs	43;"	v
-checkBoolVals	./Domain/Concrete/State.hs	260;"	v
 cntr	./Exploration/UNF/State.hs	99;"	v
 collapse	./Model/GCS.hs	84;"	v
-compute_conflicts	./Exploration/UNF/Unfolder.hs	555;"	v	file:
-cond	./Domain/Concrete/Converter.hs	44;"	v
-cond	./Domain/Interval/Converter.hs	47;"	v
-cond_transformer	./Domain/Concrete/Converter.hs	343;"	v
-cond_transformer	./Domain/Interval/Converter.hs	390;"	v
-const_transformer	./Domain/Concrete/Converter.hs	363;"	v
-const_transformer	./Domain/Interval/Converter.hs	433;"	v
+compute_conflicts	./Exploration/UNF/Unfolder.hs	561;"	v	file:
+cond	./Domain/Interval/Converter.hs	49;"	v
+cond_transformer	./Domain/Interval/Converter.hs	385;"	v
+const_transformer	./Domain/Interval/Converter.hs	428;"	v
 controlPart	./Model/GCS.hs	71;"	v
-convert	./Domain/Concrete/Converter.hs	72;"	v
-convert	./Domain/Interval/Converter.hs	67;"	v
-core	./Exploration/UNF/Unfolder.hs	688;"	v	file:
-create_thread_act	./Domain/Action.hs	46;"	v
-cst	./Domain/Concrete/Converter.hs	41;"	v
+convert	./Domain/Interval/Converter.hs	69;"	v
+core	./Exploration/UNF/Unfolder.hs	694;"	v	file:
+create_thread_act	./Domain/Action.hs	50;"	v
 cut	./Util/CmdOpts.hs	64;"	v
 cutoff	./Exploration/UNF/Cutoff/McMillan.hs	12;"	v
 cutoffCheck	./Exploration/UNF/Cutoff/McMillan.hs	22;"	v
@@ -188,27 +153,20 @@ debug_mode	./Util/CmdOpts.hs	92;"	v
 dec_evs_prefix	./Exploration/UNF/API.hs	250;"	v
 default_unf_opts	./Exploration/UNF/API.hs	32;"	v
 default_unf_stats	./Exploration/UNF/API.hs	35;"	v
-default_value	./Domain/Concrete/Converter.hs	179;"	v
-default_value	./Domain/Interval/Converter.hs	161;"	v
+default_value	./Domain/Interval/Converter.hs	157;"	v
 del_event	./Exploration/UNF/API.hs	106;"	v
 del_icnf	./Exploration/UNF/API.hs	146;"	v
 del_succ	./Exploration/UNF/API.hs	127;"	v
 disa	./Exploration/UNF/State.hs	35;"	v
 divide	./Domain/Interval/Type.hs	87;"	v
-divs	./Domain/Concrete/Converter.hs	431;"	v
-divs_conval	./Domain/Concrete/State.hs	287;"	v
 dom	./Util/CmdOpts.hs	62;"	v
-empty_state	./Domain/Concrete/State.hs	91;"	v
-empty_state	./Domain/Interval/State.hs	117;"	v
+empty_state	./Domain/Interval/State.hs	89;"	v
 enabled	./Model/GCS.hs	79;"	v
 enevs	./Exploration/UNF/State.hs	50;"	v
-eq	./Domain/Concrete/Converter.hs	438;"	v
-eq_conval	./Domain/Concrete/State.hs	313;"	v
 evts	./Exploration/UNF/State.hs	96;"	v
 execute	Main.hs	78;"	v
 execute_mode	./Util/CmdOpts.hs	79;"	v
-exit	./Domain/Concrete/Converter.hs	45;"	v
-exit_thread_act	./Domain/Action.hs	54;"	v
+exit_thread_act	./Domain/Action.hs	58;"	v
 explore	./Exploration/UNF/Unfolder.hs	68;"	v	file:
 explore	Main.hs	109;"	v
 explore_mode	./Util/CmdOpts.hs	99;"	v
@@ -216,35 +174,28 @@ ext	./Exploration/UNF/Unfolder.hs	214;"	v	file:
 extend	./Exploration/UNF/Unfolder.hs	193;"	v	file:
 filterEvent	./Exploration/UNF/API.hs	279;"	v
 filterEvents	./Exploration/UNF/API.hs	275;"	v
-fixpt	./Domain/Interval/Collapse.hs	106;"	v
-fixpt_result	./Domain/Interval/Collapse.hs	167;"	v
+fixpt	./Domain/Interval/Collapse.hs	111;"	v
+fixpt_result	./Domain/Interval/Collapse.hs	172;"	v
 frd4	./Util/Generic.hs	48;"	v
 freshCounter	./Exploration/UNF/API.hs	212;"	v
 fromBool	./Util/Generic.hs	84;"	v
 frontend	Main.hs	66;"	v
 frontend_mode	./Util/CmdOpts.hs	74;"	v
-fs_cfg	./Domain/Interval/Collapse.hs	43;"	v
-fs_cfgs	./Domain/Interval/Collapse.hs	41;"	v
-fs_mark	./Domain/Interval/Collapse.hs	44;"	v
-fs_mode	./Domain/Interval/Collapse.hs	39;"	v
-fs_symt	./Domain/Interval/Collapse.hs	42;"	v
-fs_tid	./Domain/Interval/Collapse.hs	40;"	v
+fs_cfg	./Domain/Interval/Collapse.hs	46;"	v
+fs_cfgs	./Domain/Interval/Collapse.hs	44;"	v
+fs_mark	./Domain/Interval/Collapse.hs	47;"	v
+fs_mode	./Domain/Interval/Collapse.hs	42;"	v
+fs_symt	./Domain/Interval/Collapse.hs	45;"	v
+fs_tid	./Domain/Interval/Collapse.hs	43;"	v
 fst3	./Util/Generic.hs	30;"	v
 fst4	./Util/Generic.hs	39;"	v
 gbac	./Model/GCS.hs	41;"	v
 gbst	./Model/GCS.hs	40;"	v
-gen_collapse	./Domain/Concrete/Collapse.hs	48;"	v
-gen_op	./Domain/Concrete/Converter.hs	427;"	v
-geq	./Domain/Concrete/Converter.hs	437;"	v
-geq_conval	./Domain/Concrete/State.hs	310;"	v
-get_addrs	./Domain/Concrete/Converter.hs	419;"	v
-get_addrs	./Domain/Interval/State.hs	89;"	v
-get_addrs_id	./Domain/Concrete/Converter.hs	409;"	v
-get_addrs_id	./Domain/Interval/State.hs	79;"	v
+get_addrs	./Domain/Interval/API.hs	147;"	v
+get_addrs_id	./Domain/Interval/API.hs	159;"	v
 get_alte	./Exploration/UNF/API.hs	87;"	v
 get_disa	./Exploration/UNF/API.hs	84;"	v
-get_entry	./Domain/Concrete/Converter.hs	81;"	v
-get_entry	./Domain/Interval/Converter.hs	76;"	v
+get_entry	./Domain/Interval/Converter.hs	78;"	v
 get_event	./Exploration/UNF/API.hs	65;"	v
 get_evts_of_conf	./Exploration/UNF/API.hs	352;"	v
 get_icnf	./Exploration/UNF/API.hs	81;"	v
@@ -252,138 +203,102 @@ get_name	./Exploration/UNF/API.hs	90;"	v
 get_pred	./Exploration/UNF/API.hs	75;"	v
 get_succ	./Exploration/UNF/API.hs	78;"	v
 get_tid	./Exploration/UNF/API.hs	93;"	v
-get_tid_expr	./Domain/Interval/State.hs	96;"	v
+get_tid_expr	./Domain/Interval/API.hs	132;"	v
 get_tid_sym	./Exploration/UNF/API.hs	96;"	v
-gr	./Domain/Concrete/Converter.hs	435;"	v
-gr_conval	./Domain/Concrete/State.hs	304;"	v
-h_d	./Domain/Interval/State.hs	52;"	v
-h_u	./Domain/Interval/State.hs	51;"	v
-handle_mark	./Domain/Interval/Collapse.hs	133;"	v
-heap	./Domain/Concrete/State.hs	61;"	v
-heap	./Domain/Interval/State.hs	44;"	v
-histories	./Exploration/UNF/Unfolder.hs	311;"	v	file:
-histories_lock	./Exploration/UNF/Unfolder.hs	364;"	v	file:
-history	./Exploration/UNF/Unfolder.hs	263;"	v	file:
-i	./Domain/Interval/Value.hs	49;"	v
-iDivide	./Domain/Interval/Value.hs	134;"	v
-iJoin	./Domain/Interval/Value.hs	53;"	v
-iMeet	./Domain/Interval/Value.hs	64;"	v
-i_cfgs	./Domain/Interval/Converter.hs	46;"	v
+h_d	./Domain/Interval/State.hs	65;"	v
+h_u	./Domain/Interval/State.hs	64;"	v
+handle_mark	./Domain/Interval/Collapse.hs	138;"	v
+heap	./Domain/Interval/State.hs	57;"	v
+histories	./Exploration/UNF/Unfolder.hs	315;"	v	file:
+histories_lock	./Exploration/UNF/Unfolder.hs	370;"	v	file:
+history	./Exploration/UNF/Unfolder.hs	267;"	v	file:
+i	./Domain/Interval/Value.hs	60;"	v
+iDivide	./Domain/Interval/Value.hs	145;"	v
+iJoin	./Domain/Interval/Value.hs	64;"	v
+iMeet	./Domain/Interval/Value.hs	75;"	v
+i_cfgs	./Domain/Interval/Converter.hs	48;"	v
 i_unf_state	./Exploration/UNF/API.hs	46;"	v
 icnf	./Exploration/UNF/State.hs	34;"	v
-id	./Domain/Concrete/State.hs	75;"	v
 inc_cutoffs	./Exploration/UNF/API.hs	235;"	v
 inc_evs_per_name	./Exploration/UNF/API.hs	262;"	v
 inc_evs_prefix	./Exploration/UNF/API.hs	248;"	v
 inc_max_conf	./Exploration/UNF/API.hs	228;"	v
-inc_num_th	./Domain/Concrete/State.hs	110;"	v
-inc_num_th	./Domain/Interval/State.hs	299;"	v
+inc_num_th	./Domain/Interval/API.hs	34;"	v
 inc_sum_size_max_conf	./Exploration/UNF/API.hs	254;"	v
 initial_ext	./Exploration/UNF/Unfolder.hs	43;"	v	file:
 inp	./Util/CmdOpts.hs	61;"	v
-insert_heap	./Domain/Concrete/State.hs	187;"	v
-insert_heap	./Domain/Interval/State.hs	233;"	v
-insert_heap_sigma	./Domain/Concrete/State.hs	194;"	v
-insert_local	./Domain/Concrete/State.hs	209;"	v
-insert_local	./Domain/Interval/State.hs	248;"	v
-insert_local_sigma	./Domain/Concrete/State.hs	216;"	v
-insert_thread	./Domain/Concrete/State.hs	252;"	v
-insert_thread	./Domain/Interval/State.hs	304;"	v
-interferes	./Model/GCS.hs	106;"	v
+insert_heap	./Domain/Interval/API.hs	87;"	v
+insert_local	./Domain/Interval/API.hs	103;"	v
+insert_thread	./Domain/Interval/API.hs	40;"	v
+interferes	./Model/GCS.hs	107;"	v
 interpret	Main.hs	96;"	v
 interpret_mode	./Util/CmdOpts.hs	86;"	v
-interval_diff	./Domain/Interval/Value.hs	166;"	v
-interval_diff'	./Domain/Interval/Value.hs	172;"	v
-interval_diff_eq	./Domain/Interval/Value.hs	169;"	v
-interval_div	./Domain/Interval/Value.hs	147;"	v
-interval_leq	./Domain/Interval/Converter.hs	251;"	v
+interval_diff	./Domain/Interval/Value.hs	177;"	v
+interval_diff'	./Domain/Interval/Value.hs	183;"	v
+interval_diff_eq	./Domain/Interval/Value.hs	180;"	v
+interval_div	./Domain/Interval/Value.hs	158;"	v
+interval_leq	./Domain/Interval/Converter.hs	247;"	v
 isBlocking	./Model/GCS.hs	97;"	v
 isBottom	./Model/GCS.hs	73;"	v
-isCreateOf	./Model/GCS.hs	104;"	v
-isFalse	./Domain/Concrete/State.hs	270;"	v
-isGlobal	./Model/GCS.hs	107;"	v
-isLockOf	./Model/GCS.hs	103;"	v
-isTrue	./Domain/Concrete/State.hs	263;"	v
-isUnlockOf	./Model/GCS.hs	102;"	v
-is_bot	./Domain/Concrete/State.hs	64;"	v
-is_bot	./Domain/Interval/State.hs	47;"	v
+isCreateOf	./Model/GCS.hs	105;"	v
+isGlobal	./Model/GCS.hs	108;"	v
+isJoin	./Model/GCS.hs	98;"	v
+isLockOf	./Model/GCS.hs	104;"	v
+isUnlockOf	./Model/GCS.hs	103;"	v
+is_bot	./Domain/Interval/State.hs	60;"	v
 is_causally_closed	./Exploration/UNF/API.hs	374;"	v
 is_configuration	./Exploration/UNF/API.hs	368;"	v
 is_dependent	./Exploration/UNF/API.hs	319;"	v
 is_enabled	./Model/GCS.hs	78;"	v
-is_global	./Domain/Action.hs	115;"	v
+is_global	./Domain/MemAddr.hs	80;"	v
 is_independent	./Exploration/UNF/API.hs	304;"	v
-is_live	./Domain/Interval/Collapse.hs	65;"	v
-is_locked	./Domain/Interval/Collapse.hs	56;"	v
-is_maddrs_bot	./Domain/Util.hs	64;"	v
-ite	./Domain/Interval/State.hs	212;"	v
-join_act	./Domain/Action.hs	58;"	v
-join_cstate	./Domain/Concrete/State.hs	56;"	v
-join_intheap	./Domain/Interval/State.hs	206;"	v
-join_intmcell	./Domain/Interval/State.hs	225;"	v
-join_intstate	./Domain/Interval/State.hs	194;"	v
-join_intthst	./Domain/Interval/State.hs	217;"	v
-join_intthsts	./Domain/Interval/State.hs	209;"	v
-join_maddrs	./Domain/Util.hs	78;"	v
-join_state	./Domain/Concrete/Converter.hs	57;"	v
-join_state	./Domain/Interval/Converter.hs	59;"	v
-join_thread_act	./Domain/Action.hs	50;"	v
-join_update	./Domain/Concrete/Collapse.hs	122;"	v
-join_update	./Domain/Interval/Collapse.hs	220;"	v
-land	./Domain/Concrete/Converter.hs	440;"	v
-land_conval	./Domain/Concrete/State.hs	319;"	v
-le	./Domain/Concrete/Converter.hs	434;"	v
-le_conval	./Domain/Concrete/State.hs	301;"	v
-leq	./Domain/Concrete/Converter.hs	436;"	v
-leq_conval	./Domain/Concrete/State.hs	307;"	v
-level	./Domain/Util.hs	40;"	v
+is_live	./Domain/Interval/Collapse.hs	69;"	v
+is_locked	./Domain/Interval/Collapse.hs	59;"	v
+is_maddrs_bot	./Domain/MemAddr.hs	54;"	v
+is_present	./Domain/Interval/API.hs	80;"	v
+ite	./Domain/Interval/State.hs	160;"	v
+join_act	./Domain/Action.hs	62;"	v
+join_intheap	./Domain/Interval/State.hs	154;"	v
+join_intmcell	./Domain/Interval/State.hs	173;"	v
+join_intstate	./Domain/Interval/State.hs	142;"	v
+join_intthst	./Domain/Interval/State.hs	165;"	v
+join_intthsts	./Domain/Interval/State.hs	157;"	v
+join_maddrs	./Domain/MemAddr.hs	70;"	v
+join_state	./Domain/Interval/Converter.hs	61;"	v
+join_thread_act	./Domain/Action.hs	54;"	v
+join_update	./Domain/Interval/Collapse.hs	225;"	v
+level	./Domain/MemAddr.hs	25;"	v
 list	./Util/Generic.hs	51;"	v
-locals	./Domain/Concrete/State.hs	76;"	v
-locks	./Domain/Action.hs	23;"	v
-lor	./Domain/Concrete/Converter.hs	441;"	v
-lor_conval	./Domain/Concrete/State.hs	322;"	v
-lowerBound	./Domain/Interval/Value.hs	192;"	v
+locks	./Domain/Action.hs	24;"	v
+lowerBound	./Domain/Interval/Value.hs	203;"	v
 maevs	./Exploration/UNF/State.hs	49;"	v
 main	Main.hs	49;"	v
 main_tid	./Model/GCS.hs	59;"	v
-meet_maddrs	./Domain/Util.hs	70;"	v
-minus	./Domain/Concrete/Converter.hs	445;"	v
-minus_conval	./Domain/Concrete/State.hs	293;"	v
-modify_heap	./Domain/Concrete/State.hs	200;"	v
-modify_heap	./Domain/Interval/State.hs	239;"	v
-modify_local_sigma	./Domain/Concrete/State.hs	241;"	v
-modify_state	./Domain/Concrete/State.hs	228;"	v
-modify_state	./Domain/Interval/State.hs	260;"	v
-mtrace	./Domain/Interval/State.hs	28;"	v
+meet_maddrs	./Domain/MemAddr.hs	61;"	v
+modify_heap	./Domain/Interval/API.hs	93;"	v
+mtrace	./Domain/Interval/API.hs	28;"	v
 mulIVal	./Domain/Interval/Type.hs	48;"	v
-mult	./Domain/Concrete/Converter.hs	430;"	v
-multValue	./Domain/Interval/Value.hs	100;"	v
-mult_conval	./Domain/Concrete/State.hs	284;"	v
+multValue	./Domain/Interval/Value.hs	111;"	v
 mytrace	./Util/Generic.hs	15;"	v
 name	./Exploration/UNF/State.hs	30;"	v
-negExp	./Domain/Interval/Converter.hs	478;"	v
-negOp	./Domain/Interval/Converter.hs	486;"	v
-neg_conval	./Domain/Concrete/State.hs	298;"	v
-neg_tr	./Domain/Concrete/Converter.hs	446;"	v
+negExp	./Domain/Interval/Converter.hs	461;"	v
+negOp	./Domain/Interval/Converter.hs	469;"	v
 negateIVal	./Domain/Interval/Type.hs	81;"	v
-negateValue	./Domain/Interval/Value.hs	126;"	v
-neq	./Domain/Concrete/Converter.hs	439;"	v
-neq_conval	./Domain/Concrete/State.hs	316;"	v
+negateValue	./Domain/Interval/Value.hs	137;"	v
 nr_cutoffs	./Exploration/UNF/State.hs	84;"	v
 nr_evs_per_name	./Exploration/UNF/State.hs	87;"	v
 nr_evs_prefix	./Exploration/UNF/State.hs	85;"	v
 nr_max_conf	./Exploration/UNF/State.hs	83;"	v
-num_th	./Domain/Concrete/State.hs	63;"	v
-num_th	./Domain/Interval/State.hs	46;"	v
+num_th	./Domain/Interval/State.hs	59;"	v
+offset	./Domain/MemAddr.hs	24;"	v
 op_evs_prefix	./Exploration/UNF/API.hs	242;"	v
 opts	./Exploration/UNF/State.hs	101;"	v
 partition_dependent	./Exploration/UNF/API.hs	288;"	v
 pcnf	./Exploration/UNF/State.hs	97;"	v
 plusIVal	./Domain/Interval/Type.hs	40;"	v
-plusValue	./Domain/Interval/Value.hs	89;"	v
+plusValue	./Domain/Interval/Value.hs	100;"	v
 pop	./Exploration/UNF/API.hs	205;"	v
-pos	./Domain/Concrete/State.hs	74;"	v
-possible_altes	./Exploration/UNF/Unfolder.hs	591;"	v	file:
+possible_altes	./Exploration/UNF/Unfolder.hs	597;"	v	file:
 pred	./Exploration/UNF/State.hs	32;"	v
 predecessorWith	./Exploration/UNF/API.hs	382;"	v
 predecessors	./Exploration/UNF/API.hs	332;"	v
@@ -391,45 +306,35 @@ prime	Main.hs	144;"	v
 prime_mode	./Util/CmdOpts.hs	107;"	v
 print_stats	./Exploration/UNF/State.hs	128;"	v
 prog_modes	./Util/CmdOpts.hs	130;"	v
-prune	./Exploration/UNF/Unfolder.hs	697;"	v	file:
-prune_config	./Exploration/UNF/Unfolder.hs	679;"	v	file:
+prune	./Exploration/UNF/Unfolder.hs	703;"	v	file:
+prune_config	./Exploration/UNF/Unfolder.hs	685;"	v	file:
 push	./Exploration/UNF/API.hs	198;"	v
-rds	./Domain/Action.hs	21;"	v
-read_act	./Domain/Action.hs	40;"	v
-read_memaddr	./Domain/Interval/State.hs	284;"	v
-read_memaddrs	./Domain/Interval/State.hs	278;"	v
+rds	./Domain/Action.hs	22;"	v
+read_act	./Domain/Action.hs	41;"	v
+read_memory	./Domain/Interval/API.hs	61;"	v
+read_memory_addr	./Domain/Interval/API.hs	67;"	v
 reset_alte	./Exploration/UNF/API.hs	182;"	v
-rmdr	./Domain/Concrete/Converter.hs	432;"	v
-rmdr_conval	./Domain/Concrete/State.hs	290;"	v
 runOption	Main.hs	54;"	v
 safeLookup	./Util/Generic.hs	72;"	v
-scope	./Domain/Concrete/Converter.hs	39;"	v
-scope	./Domain/Interval/Converter.hs	43;"	v
+scope	./Domain/Interval/Converter.hs	45;"	v
 seed	./Util/CmdOpts.hs	62;"	v
 separator	./Exploration/UNF/Unfolder.hs	59;"	v	file:
 set_cutoff_table	./Exploration/UNF/API.hs	221;"	v
 set_disa	./Exploration/UNF/API.hs	165;"	v
 set_event	./Exploration/UNF/API.hs	102;"	v
 set_pcnf	./Exploration/UNF/API.hs	190;"	v
-set_pos	./Domain/Concrete/State.hs	95;"	v
-set_pos	./Domain/Interval/State.hs	128;"	v
-set_pos_s	./Domain/Concrete/State.hs	98;"	v
+set_pos	./Domain/Interval/API.hs	121;"	v
 set_previous_disa	./Exploration/UNF/API.hs	359;"	v
-set_single_state	./Domain/Concrete/Converter.hs	65;"	v
-set_state	./Domain/Concrete/Converter.hs	52;"	v
-set_state	./Domain/Interval/Converter.hs	54;"	v
+set_state	./Domain/Interval/Converter.hs	56;"	v
 showEvents	./Exploration/UNF/State.hs	121;"	v
-showIntHeap	./Domain/Interval/State.hs	62;"	v
-showResultList	./Domain/Interval/Collapse.hs	50;"	v
-showThState	./Domain/Interval/State.hs	109;"	v
-showThStates	./Domain/Interval/State.hs	106;"	v
+showMem	./Domain/Interval/State.hs	75;"	v
+showResultList	./Domain/Interval/Collapse.hs	53;"	v
+showThStates	./Domain/Interval/State.hs	77;"	v
 signumIVal	./Domain/Interval/Type.hs	76;"	v
 simple_run	./Model/GCS.hs	93;"	v
-single_edge	./Domain/Concrete/Collapse.hs	59;"	v
 snd3	./Util/Generic.hs	33;"	v
 snd4	./Util/Generic.hs	42;"	v
-st	./Domain/Concrete/Converter.hs	40;"	v
-st	./Domain/Interval/Converter.hs	44;"	v
+st	./Domain/Interval/Converter.hs	46;"	v
 stak	./Exploration/UNF/State.hs	98;"	v
 stas	./Exploration/UNF/State.hs	100;"	v
 state	./Exploration/UNF/State.hs	48;"	v
@@ -438,65 +343,52 @@ stats	./Exploration/UNF/State.hs	102;"	v
 stf	./Util/CmdOpts.hs	64;"	v
 stid	Main.hs	160;"	v
 stid_mode	./Util/CmdOpts.hs	115;"	v
-strong_update	./Domain/Concrete/Collapse.hs	136;"	v
-strong_update	./Domain/Interval/Collapse.hs	234;"	v
-sts	./Domain/Concrete/State.hs	52;"	v
-sub	./Domain/Concrete/Converter.hs	429;"	v
+strong_update	./Domain/Interval/Collapse.hs	239;"	v
 subIVal	./Domain/Interval/Type.hs	62;"	v
-subValue	./Domain/Interval/Value.hs	116;"	v
-sub_conval	./Domain/Concrete/State.hs	281;"	v
+subValue	./Domain/Interval/Value.hs	127;"	v
 subsumes	./Model/GCS.hs	72;"	v
-subsumes_concrete	./Domain/Concrete/State.hs	121;"	v
-subsumes_interval	./Domain/Interval/State.hs	143;"	v
+subsumes_interval	./Domain/Interval/State.hs	98;"	v
 succ	./Exploration/UNF/State.hs	33;"	v
 successors	./Exploration/UNF/API.hs	341;"	v
 sum_size_max_conf	./Exploration/UNF/State.hs	86;"	v
-sym	./Domain/Concrete/Converter.hs	42;"	v
-sym	./Domain/Interval/Converter.hs	45;"	v
+sym	./Domain/Interval/Converter.hs	47;"	v
 symt	./Model/GCS.hs	43;"	v
 syst	./Exploration/UNF/State.hs	95;"	v
 tcnt	./Model/GCS.hs	45;"	v
-tcreate	./Domain/Action.hs	25;"	v
+tcreate	./Domain/Action.hs	26;"	v
 test	Main.hs	189;"	v
 test_mode	./Util/CmdOpts.hs	127;"	v
-texit	./Domain/Action.hs	27;"	v
-th_cfg_id	./Domain/Interval/State.hs	71;"	v
-th_locals	./Domain/Interval/State.hs	72;"	v
-th_pos	./Domain/Interval/State.hs	70;"	v
-th_states	./Domain/Concrete/State.hs	62;"	v
-th_states	./Domain/Interval/State.hs	45;"	v
+texit	./Domain/Action.hs	28;"	v
+th_cfg_id	./Domain/Interval/State.hs	43;"	v
+th_locals	./Domain/Interval/State.hs	44;"	v
+th_pos	./Domain/Interval/State.hs	42;"	v
+th_states	./Domain/Interval/State.hs	58;"	v
 thds	./Model/GCS.hs	44;"	v
-tjoin	./Domain/Action.hs	26;"	v
+tjoin	./Domain/Action.hs	27;"	v
 toBool	./Util/Generic.hs	79;"	v
 toThCFGSym	./Model/GCS.hs	75;"	v
-top_interval	./Domain/Interval/Value.hs	46;"	v
-transformer	./Domain/Concrete/Converter.hs	214;"	v
-transformer	./Domain/Interval/Converter.hs	258;"	v
-transformer_decl	./Domain/Concrete/Converter.hs	103;"	v
-transformer_decl	./Domain/Interval/Converter.hs	98;"	v
-transformer_decls	./Domain/Concrete/Converter.hs	98;"	v
-transformer_decls	./Domain/Interval/Converter.hs	93;"	v
-transformer_expr	./Domain/Concrete/Converter.hs	187;"	v
-transformer_expr	./Domain/Interval/Converter.hs	168;"	v
-transformer_init	./Domain/Concrete/Converter.hs	140;"	v
-transformer_init	./Domain/Interval/Converter.hs	122;"	v
+top_interval	./Domain/Interval/Value.hs	57;"	v
+transformer	./Domain/Interval/Converter.hs	254;"	v
+transformer_decl	./Domain/Interval/Converter.hs	100;"	v
+transformer_decls	./Domain/Interval/Converter.hs	95;"	v
+transformer_expr	./Domain/Interval/Converter.hs	164;"	v
+transformer_init	./Domain/Interval/Converter.hs	124;"	v
 trd3	./Util/Generic.hs	36;"	v
 trd4	./Util/Generic.hs	45;"	v
 unfold	./Exploration/UNF/Unfolder.hs	132;"	v	file:
 unfolder	./Exploration/UNF/Unfolder.hs	23;"	v
-unlocks	./Domain/Action.hs	24;"	v
-unop_transformer	./Domain/Concrete/Converter.hs	369;"	v
-unop_transformer	./Domain/Interval/Converter.hs	440;"	v
-up_pc	./Domain/Interval/Collapse.hs	128;"	v
-update_conmcell	./Domain/Concrete/State.hs	205;"	v
-update_conmcell	./Domain/Interval/State.hs	244;"	v
-update_node_table	./Domain/Interval/Collapse.hs	121;"	v
-update_pc	./Domain/Interval/State.hs	121;"	v
-upperBound	./Domain/Interval/Value.hs	187;"	v
-var_transformer	./Domain/Concrete/Converter.hs	387;"	v
-var_transformer	./Domain/Interval/Converter.hs	457;"	v
-widening	./Domain/Interval/Value.hs	198;"	v
-worklist	./Domain/Interval/Collapse.hs	180;"	v
-worklist_fix	./Domain/Concrete/Collapse.hs	82;"	v
-write_act	./Domain/Action.hs	43;"	v
-wrs	./Domain/Action.hs	22;"	v
+unlocks	./Domain/Action.hs	25;"	v
+unop_transformer	./Domain/Interval/Converter.hs	435;"	v
+up_pc	./Domain/Interval/Collapse.hs	133;"	v
+update_node_table	./Domain/Interval/Collapse.hs	126;"	v
+update_pc	./Domain/Interval/API.hs	114;"	v
+upperBound	./Domain/Interval/Value.hs	198;"	v
+var_transformer	./Domain/Interval/Converter.hs	452;"	v
+widening	./Domain/Interval/Value.hs	209;"	v
+worklist	./Domain/Interval/Collapse.hs	185;"	v
+write_act	./Domain/Action.hs	44;"	v
+write_act_addr	./Domain/Action.hs	47;"	v
+write_memory	./Domain/Interval/API.hs	47;"	v
+write_memory_addr	./Domain/Interval/API.hs	54;"	v
+wrs	./Domain/Action.hs	23;"	v
+zero	./Domain/Interval/Value.hs	44;"	v