1 # ifndef F_EMPSET_H
2 # define F_EMPSET_H
3 
4 # include "eref.h"
5 # include "erc.h"
6 # include "ereftab.h"
7 
8 typedef erc empset;
9 
10 /*
11   Abstraction function, toEmpSet:
12     e \in toEmpSet(s) ==
13       exists er (count(er, s.val) = 1
14         /\ getERef(known, e) = er)
15 
16   Rep invariant:
17     forall s: empset
18       (forall er: eref (count(er, s.val) <= 1)
19       /\ s.activeIters = 0
20       /\ forall er: eref (count(er, s.val) = 1
21         => in(known, er)))
22 */
23 
24 # include "empset.lh"
25 
26 # define empset_create()  (erc_create())
27 # define empset_final(s) (erc_final(s))
28 # define empset_size(es) (erc_size(es))
29 # define empset_choose(es) (eref_get(erc_choose(es)))
30 # define empset_sprint(es) (erc_sprint(es))
31 
32 #define empset_elements(e, m_x) \
33    erc_elements(e, m_y) { employee m_x = eref_get(m_y);
34 #define end_empset_elements        } end_erc_elements
35 
36 # endif
37