% set of locations 
locations(['FF', 'FE', 'FF1', 'FE1', 'A','B', 'BF','BE','X', 'Y']).

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

ghost_location(['X']).

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

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

% set of data selector edges
data_selectors(['val']).

% unfold predicates : (enablingNode, edges, constraints, vanishingNode)
unfoldPred('FF','X',[in('FF','X'), out('FE','FE')],[(eq, ('X', next), 'FF'), (lt, ('X', val), ('FF', val))],[]).
unfoldPred('FF','X',[in('FF','X'),out('FE','X')],[(eq, ('X', val), ('FF', val))],['FE']).

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



% input states : (ScenarioId, variable and selector predicate assignments)
input_state(0,[(eq,head,'FF'), (eq, y, 'Y'), (eq, ('FE', next), 'A'), (eq, ('A', next), 'Y'), (eq, ('Y',next), 'B'), (eq, ('B', next), 'BF'), (eq, ('BE', next), 'EMP'), (eq, ('X', next), 'UNDEFINED'), (eq, ('FF', val), '1'), (eq, ('FE', val), '2'), (eq, ('A', val), '3'), (eq, ('B', val), '5'), (eq, ('Y', val), '4'), (eq, ('BF', val), '6'), (eq, ('BE', val), '7')]).

% input states : (ScenarioId, variable and selector predicate assignments)
input_state(1,[(eq, head,'Y'), (eq, y, 'Y'), (eq, ('Y',next), 'B'),(eq, ('B', next), 'BF'), (eq, ('BE', next), 'EMP'), (eq, ('B', val), '5'), (eq, ('Y', val), '4'), (eq, ('BF', val), '6'), (eq, ('BE', val), '7')]).

input_state(2,[(eq, head,'A'), (eq, y, 'Y'), (eq, ('A', next), 'Y'), (eq, ('Y',next), 'EMP'), (eq, ('A', val), '3'), (eq, ('Y', val), '4')]).

input_state(3,[(eq, head,'Y'), (eq, ('Y',next), 'EMP'), (eq, y, 'Y'), (eq, ('Y', val), '4')]).

% output states : (ScenarioId, variable and selector predicate assignments)
output_state(0,[(eq, y, 'Y'), (eq, ('FE1', next), 'A'), (eq, ('A', next), 'B'), (eq, ('B', next), 'BF'), (eq, ('BE', next), 'EMP'), (eq, ('X', next), 'UNDEFINED'),(eq, ('FE', next),'UNDEFINED')]).


% output states : (ScenarioId, variable and selector predicate assignments)
output_state(1,[(eq, head, 'B'),(eq, y, 'Y'), (eq, ('B', next), 'BF'), (eq, ('BE', next), 'EMP'), (eq, ('X', next), 'UNDEFINED'),(eq, ('FE', next),'UNDEFINED')]).

output_state(2,[(eq, head, 'A'),(eq, y, 'Y'),(eq, ('A', next), 'EMP'),(eq, ('X', next), 'UNDEFINED'),(eq, ('FE', next),'UNDEFINED')]).

output_state(3,[(eq,head, 'EMP'),(eq, y, 'Y')]).

% intermediate state constraints : (ScenarioId, LocationId, variable and selector predicate assignments)
intermediate_state(0, 8, [(eq, y,'Y'), (eq, temp1, 'A'), (eq, temp2, 'Y'),(eq, ('FE1', next), 'A'), (eq, ('A', next),'Y'),(eq, ('Y',next), 'B'), (eq, ('B', next), 'BF'), (eq, ('BE', next),'EMP'), (eq, ('FE', next),'UNDEFINED')]).

% number of scenarios
num_scenarios(4).

% 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, f8, 8, negcond).
cfg_edge(3, f3, 4, unfold).
cfg_edge(4, f4, 5, assign).
cfg_edge(5, f5, 6, assign).
cfg_edge(6, f6, 2, fold).
cfg_edge(8, f9, 9, cassign).
cfg_edge(9, f10, 10, cassign).
cfg_edge(10, f11, 11, cassign).
cfg_edge(11, f12, 12, cassign).


% start location of cfg
start_location(1).

% return location of cfg
return_location(12).

% loop location in cfg
loop_location(2).
