% set of locations 
locations(['TR','TB','TR1','TB1', 'Y']).

% locations introduced by unfold operation
ghost_location(['Y']).

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

% set of program variables
variables(['root','temp1']).

constant_variables([x]).

% set of selector edges in the program
selectors(['left', 'right']).

data_selectors(['val']).

% unfold predicates : (enablingNode, replacementNode, edges, constraints, vanishingNode)
unfoldPred('TR', 'Y', [in('TR','Y')],[(eq, ('Y', val), x), (eq, ('Y', left), 'UNDEFINED'), (eq, ('Y', right), 'UNDEFINED')],[]).
unfoldPred('TR', 'Y', [in('TR','Y')],[(eq, ('Y', val), 3), (eq,('Y',left),'TR'), (eq, ('Y',right), 'UNDEFINED')],[]).
unfoldPred('TR', 'Y', [in('TR','Y')],[(eq, ('Y', val), 1), (eq,('Y',right),'TR'), (eq, ('Y',left), 'UNDEFINED')],[]).


% fold predicates : (enablingNode, replacementNode, edges, constraints, vanishingNode)
foldPred('Y', 'TB1', [in('Y','TB1'),out('Y','TB1')],[(eq, ('Y', left), 'UNDEFINED'),(eq, ('Y', right), 'TR'),(eq, ('TB1', left), 'UNDEFINED'), (eq, ('TB1', right), 'UNDEFINED')],['Y']).
foldPred('Y', 'TB1', [in('Y','TB1'),out('Y','TB1')],[(eq, ('Y', right), 'UNDEFINED'),(eq, ('Y', left), 'TR'),(eq, ('TB1', left), 'UNDEFINED'), (eq, ('TB1', right), 'UNDEFINED')],['Y']).
foldPred('Y', 'TB1', [in('Y','TB1'),out('Y','TB1')],[(eq, ('Y', right), 'UNDEFINED'),(eq, ('Y', left), 'UNDEFINED'),(eq, ('TB1', left), 'UNDEFINED'), (eq, ('TB1', right), 'UNDEFINED')],['Y']).


foldPred('Y', 'TB1', [out('Y','TB1')],[(eq, ('Y', left), 'UNDEFINED'),(eq, ('Y', right), 'TR'),or([(neq, ('TB1', left), 'UNDEFINED')], [(neq, ('TB1', right), 'UNDEFINED')])],['Y']).
foldPred('Y', 'TB1', [out('Y','TB1')],[(eq, ('Y', right), 'UNDEFINED'),(eq, ('Y', left), 'TR'),or([(neq, ('TB1', left), 'UNDEFINED')], [(neq, ('TB1', right), 'UNDEFINED')])],['Y']).
foldPred('Y', 'TB1', [out('Y','TB1')],[(eq, ('Y', left), 'UNDEFINED'),(eq, ('Y', right), 'UNDEFINED'),or([(neq, ('TB1', left), 'UNDEFINED')], [(neq, ('TB1', right), 'UNDEFINED')])],['Y']).


% input states : (ScenarioId, variable and selector predicate assignments)
input_state(0,[(eq, root, 'TR'), (eq, x, 2)]).


% output states : (ScenarioId, variable and selector predicate assignments)
output_state(0,[(eq, (temp1, val), x)]).


% number of scenarios
num_scenarios(1).

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


% 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, cassign).
cfg_edge(5, f5, 6, cassign).
cfg_edge(6, f6, 7, cassign).
cfg_edge(7, f7, 2, fold).

% start location of cfg
start_location(1).

% return location of cfg
return_location(8).

% loop location in cfg
loop_location(2).
