% set of locations 
locations(['A','B','MIDF','MIDE', 'MID1F','MID1E','X']).

% set of summary nodes on which selector operation would cause error
summary_nodes(['MID1F', 'MIDF']).

ghost_location(['X']).

% set of program variables
variables(['head','temp1','temp2','temp3']).

% set of selector edges in the program
selectors(['next']).

% unfold predicates : (enablingNode, edges, constraints, vanishingNode)
unfoldPred('MIDF','X',[in('MIDF','X'), out('MIDE','MIDE')],[(eq, ('X', next), 'MIDF')],[]).
unfoldPred('MIDF','X',[in('MIDF','X'),out('MIDE','X')],[],['MIDE']).

% fold predicates : (enablingNode, edges, constraints, vanishingNode)
foldPred('X', 'MID1E', [in('X','MID1F'),out('X','MID1E')],[(eq, ('MID1E', next), 'UNDEFINED')],['X']).
foldPred('X', 'MID1E', [in('MID1F','MID1F'), out('X','MID1E')],[(eq, ('MID1E', next), 'X')], ['X']).



% input states : (ScenarioId, variable and selector predicate assignments)
input_state(0,[(eq, head,'A'), (eq, ('A', next),'MIDF'),(eq, ('MIDE', next),'B'), (eq, ('B', next), 'EMP'), (eq, ('MID1E', next),'UNDEFINED'), (eq, ('X', next), 'UNDEFINED')]).

% output states : (ScenarioId, variable and selector predicate assignments)
output_state(0,[(eq, head, 'B'), (eq, ('A', next),'EMP'), (eq, ('B', next), 'MID1F'), (eq, ('X', next),'UNDEFINED'), (eq, ('MIDE', next),'UNDEFINED'), (eq, ('MID1E', next), 'A')]).

% intermediate state constraints : (ScenarioId, LocationId, variable and selector predicate assignments)
intermediate_state(0, 9, [(eq, temp1,'EMP'),(eq, temp2, 'B'), (eq, temp3, 'MID1E'), (eq, ('A', next),'MID1F'), (eq, ('B', next), 'EMP'), (eq, ('X', next),'UNDEFINED'), (eq, ('MIDE', next),'UNDEFINED'), (eq, ('MID1E', next), 'B')]).

% number of scenarios
num_scenarios(1).

% number of unrollings for reaching fixpoint
num_unrollings(4).


% define the control flow graph
% cfg_edge(FromLoc, FId, ToLoc, TypeStmt)

cfg_edge(1, f1, 2, assign).
cfg_edge(2, f2, 3, cond).
cfg_edge(2, f10, 9, negcond).
cfg_edge(3, f3, 4, unfold).
cfg_edge(4, f4, 5, assign).
cfg_edge(5, f5, 6, assign).
cfg_edge(6, f6, 7, assign).
cfg_edge(7, f7, 8, assign).
cfg_edge(8, f9, 2, fold).
cfg_edge(9, f11, 10, assign).
cfg_edge(10, f12, 11, assign).
cfg_edge(11, f13, 12, assign).
cfg_edge(12, f14, 13, assign).
cfg_edge(13, f15, 14, cassign).

% start location of cfg
start_location(1).

% return location of cfg
return_location(13).

% loop location in cfg
loop_location(2).
