function semanticTranslation( chart, ha, modelName, optEagerViolation )
%SEMANTICTRANSLATION Model translation with semantics preservation.
% Each location instantiates a location pattern for the Stateflow model.
% Similarly, each transition instantiates a transition pattern. First the
% location patterns are created, since (chicken or the egg dilemma) the
% transitions connect the resulting states/junctions.
%
% ------------------------------------------------------------------------------
% author: Christian Schilling
% ------------------------------------------------------------------------------

    % Set this option to add epsilons to bounds to prevent intersections only at
    % a point. This case is not handled correctly by Stateflow, as it is very
    % unlikely to find this point.
    % The size of epsilon is a model parameter and can be controlled by the
    % user.
    IS_ADD_EPS = true;
    
    % position parameters for locations and junctions
    POS = struct('X0', 50, 'Y0', 50, 'W', 200, 'H', 150, 'J_H', 0);
    POS.J_H = 0.3 * POS.H;

    % variables, locations, transitions
    VARS = ha.variableNames;
    LOCS = ha.modes;
    TRANS = ha.transitions;
    
    % Java printer
    printer = com.verivital.hyst.printers.StateflowSpPrinter(VARS, IS_ADD_EPS);
    
    % maximum number of outgoing transitions for any state (pdated later)
    numTransMax = 0;
    
    % mapping from location name to location ID
    % NOTE: The ID is assigned here, so there is no correllation with the
    % SpaceEx ID.
    loc2id = java.util.LinkedHashMap(LOCS.size()); % TODO: please map back, use e.g., ha.modeNamesToIds
    
    % mapping from location ID to the following data:
    % - location name
    % - entry state
    % - junction for leaving dwell-state
    % - outgoing transitions (possibly empty)
    % - initial condition (possibly empty)
    id2data = ...
        struct('state', [], 'junction', [], 'trans', []);
    id2data.state = cell(LOCS.size(), 1);
    id2data.junction = cell(LOCS.size(), 1);
    id2data.trans = cell(LOCS.size(), 1);
    
    % fill loc2id and names
    locId = 0;
    itLoc = LOCS.values().iterator();
    while (itLoc.hasNext())
        locName = itLoc.next().name;
        locId = locId + 1;
        loc2id.put(locName, locId);
        id2data.trans{locId} = java.util.LinkedList();
    end
    % fill outgoing transitions
    itTrans = TRANS.iterator();
    while (itTrans.hasNext())
        trans = itTrans.next();
        sourceId = loc2id.get(trans.from.name);
        id2data.trans{sourceId}.add(trans);
    end
    
    %ha.modeNamesToIds = loc2id;
    
    % --- add chart components (states, junctions, and transitions) ---
    
    % add initial state
    state_init = addStateInit();
    initIdx = 1;
    
    % iterate over all locations
    locId = 0;
    itLoc = LOCS.values().iterator();
    while (itLoc.hasNext())
        % get location
        loc = itLoc.next();
        locId = locId + 1;
        
        % get outgoing transitions
        numTransOut = id2data.trans{locId}.size();
        numTransMax = max(numTransMax, numTransOut);
        
        % add entry state
        state_in = addStateIn(loc, locId, numTransOut);
        
        % put state into mapping
        id2data.state{locId} = state_in;
        
        % add the transition 'initial state -> entry state' (if location is initial)
        initIdx = addTransitionInitial(loc, state_init, state_in, initIdx);
        
        % add junction for choosing transitions
        junction_in2dwell = addJunctionIn2dwell(state_in.Position);
        
        % add transition 'entry state -> transition choosing junction'
        addTransitionIn2choose(state_in, junction_in2dwell);
        
        % add dwelling state
        state_dwell = addStateDwell(loc, state_in, numTransOut);
        
        % add junction for leaving dwell state
        junction_dwell2next = addJunctionDwell2next(state_dwell.Position);
        id2data.junction{locId} = junction_dwell2next;
        
        % add transition 'dwell state -> leave junction'
        addTransitionDwell2leave(state_dwell, junction_dwell2next);
        
        % add junction for backtracking
        junction_dwell2choose = addJunctionDwell2choose(state_dwell.Position);
        
        % add transition 'dwell state -> backtrack junction'
        addTransitionDwell2backtrack(state_dwell, junction_dwell2choose, ...
            loc, optEagerViolation);
        
        % add transition 'leave junction -> dwell state'
        addTransitionLeave2dwell(junction_dwell2next, state_dwell);
        
        % extra handling in case there are outgoing transitions
        if (numTransOut > 0)
            % add dwelling time choosing state
            state_choose = addStateChoose(loc, state_in.Position);
            
            % add transition 'choosing state -> dwelling state'
            addTransitionChoose2dwell(state_choose, state_dwell);
            
            % add transition 'transition choosing junction -> choosing state'
            addTransitionChooseJ2choose(junction_in2dwell, state_choose);
            
            % add transition 'choosing state -> transition choosing junction'
            addTransitionChoose2chooseJ(state_choose, junction_in2dwell);
            
            % add transition 'time choosing junction -> dwelling state'
            addTransitionChooseTime2dwell(junction_dwell2choose, state_choose);
        end
        
        % add transition 'entry junction -> dwelling state'
        addTransitionInJ2dwell(junction_in2dwell, state_dwell);
        
        % add transition 'backtracking junction -> dwelling state'
        addTransitionBacktrack2dwell(junction_dwell2choose, state_dwell);
    end
    
    % subtract 1, as it was incremented k times for k initial transitions, but
    % started with value '1'
    initIdx = initIdx - 1;
    
    % For adding the original transitions, we need to have all states created.
    % So we start a new loop here to add the regular transitions.
    for locId = 1 : LOCS.size()
        junction_dwell2next = id2data.junction{locId};
        juncX = junction_dwell2next.Position.Center(1);
        juncY = junction_dwell2next.Position.Center(2);
        
        % add a junction for each (original) transition
        iTrans = 0;
        transIt = id2data.trans{locId}.iterator();
        while (transIt.hasNext())
            iTrans = iTrans + 1;
            % add junction for taking (original) transition
            junction_trans = addJunctionTrans(juncX, juncY, iTrans);
            
            % add transition 'leaving junction -> transition junction'
            addTransitionLeave2trans(junction_dwell2next, junction_trans, iTrans);
            
            % add transition 'transition junction -> entry state'
            % = original transition
            trans = transIt.next();
            targetLoc = trans.to;
            targetId = loc2id.get(targetLoc.name);
            state_in = id2data.state{targetId};
            addTransitionTrans2in(junction_trans, state_in, trans, juncX);
        end
    end
    
    % add initial transition
    addTransitionInit2in(state_init, numTransMax, initIdx);
    
    % --- add outer components and variables ---
    
    CHART_NAME = chart.Name;
    
    % add (translation-related) auxiliary variables
    addAuxiliaryVariables(chart, printer, numTransMax);
    
    % add stop block
    add_block('built-in/Stop', [modelName '/Stop'], ...
        'Position', [450, 0, 500, 50]);
    line = ...
        add_line(modelName, [CHART_NAME, '/1'], 'Stop/1', 'autorouting', 'on');
    set_param(line, 'Name', 'stop');
    
    % add random number block
    % This is used for choosing a random number.
    addRandomBlock(printer, [modelName '/RandNum'], [25, 125, 75, 175], '0', ...
        '1');
    line = add_line(modelName, 'RandNum/1', [CHART_NAME, '/1'], ...
        'autorouting', 'on');
    set_param(line, 'Name', 'randNum');
    
    % add random array block
    % This is used for choosing the next outgoing transition.
    % It is only added in case there are any outgoing transitions in the model.
    if (numTransMax > 0)
        total = num2str(numTransMax + 1);
        minString = '[1';
        minAddString = ', 1';
        maxString = ['[', total];
        maxAddString = [', ', total];
        for i = 2 : numTransMax
            minString = [minString, minAddString];
            maxString = [maxString, maxAddString];
        end
        minString = [minString, ']'];
        maxString = [maxString, ']'];
        
        addRandomBlock(printer, [modelName '/RandArr'], [25, 200, 75, 250], ...
            minString, maxString);
        line = add_line(modelName, 'RandArr/1', [CHART_NAME, '/2'], ...
            'autorouting', 'on');
        set_param(line, 'Name', 'randArr');
    end
    
    % number of auxiliary variables linked to scope
    SCOPE_OFFSET = 3;
    
    % add scope block
    add_block('built-in/Scope', [modelName '/Scope'], ...
        'NumInputPorts', num2str(VARS.size() + SCOPE_OFFSET), ...
        'Position', [450, 75, 500, 150], ...
        'SaveToWorkspace', 'on', ...
        'SaveName', 'ScopeData', ...
        'DataFormat', 'Structure', ...
        'LimitDataPoints', 'off');
    
    % link time variable and backtracking information to scope
    linkToScope(modelName, CHART_NAME, 2, 1, 'time');
    linkToScope(modelName, CHART_NAME, 3, 2, 'backtrack');
    linkToScope(modelName, CHART_NAME, 4, 3, 'location');
    
    % string constants for variables
    PREFIX_VARIABLE = char(printer.PREFIX_VARIABLE);
    PREFIX_ASSIGNMENT = char(printer.PREFIX_ASSIGNMENT);
    PREFIX_OUTPUT = char(printer.PREFIX_OUTPUT);
    
    % create local and output variables
    i = SCOPE_OFFSET;
    itVar = VARS.iterator();
    while (itVar.hasNext())
        variable = itVar.next();
        i = i + 1;
        
        % original variable
        var = addVariable(chart, [PREFIX_VARIABLE, variable], 'Local', ...
            'CONTINUOUS');
        var.Props.Array.Size = '';
        
        % temporary variable
        addVariable(chart, [PREFIX_ASSIGNMENT, variable], 'Local', 'DISCRETE');
        
        % output variable
        addVariable(chart, [PREFIX_OUTPUT, variable], 'Output', 'DISCRETE');
        
        % link the output to scope
        linkToScope(modelName, CHART_NAME, i + 1, i, variable);
    end
    
    % add constants
    addConstants(chart, ha.constants, PREFIX_VARIABLE);
    
    % set simulation time to infinity
    set_param(modelName, 'StopTime', 'inf');
    
    
    % ---
    % --- nested functions for adding states, junctions, and transitions ---
    % ---
    
    
    function [ state ] = addStateInit()
        state = addState(chart, 'init', [0, 0, 30, 20]);
    end
    
    function [ state ] = addStateIn( loc, locId, numTransOut )
    % adds an entry state
    % - stores variables to temporary variables
    % - constructs new transition array
    % - resets transition array index
    
        label = char(printer.getStateInLabel(loc, locId, numTransOut));
        state = addState(chart, label, ...
            [POS.X0 + (2 * locId * POS.W), POS.Y0, POS.W, POS.H]);
    end
    
    function [ state ] = addStateDwell( loc, state_in, numTransOut )
    % adds a dwell-state
    % - dwell until either the dwelling time is reached and a transition is
    %   enabled or until the invariant is violated
    
        % determine the state position depending on outgoing transitions
        if (numTransOut > 0)
            % outgoing transitions, put another state in between later on
            dwellY = 4*POS.H;
        else
            % no outgoing transitions, put state directly below
            dwellY = 2*POS.H;
        end
        
        label = char(printer.getStateDwellLabel(loc));
        state = addState(chart, label, state_in.Position + [0, dwellY, 0, 0]);
    end
    
    function [ state ] = addStateChoose( loc, state_inPos )
    % adds a state choosing the dwelling time
    % - restores the variables (backtracking)
    % - chooses the next dwelling time
    
        label = char(printer.getStateChooseLabel(loc));
        state = addState(chart, label, state_inPos + [0, 2 * POS.H, 0, 0]);
    end
    
    function [ junction ] = addJunctionIn2dwell( state_inPos )
    % adds a junction for choosing transitions
    % - goes to choose-state when there are transitions left
    % - goes to dwell-state when there are no transitions left
    
        junction = addJunction(chart, ...
            [state_inPos(1) + POS.W * 0.5, state_inPos(2) + POS.H + POS.J_H]);
    end
    
    function [ junction ] = addJunctionDwell2next( state_dwellPos )
    % adds a junction for leaving the dwell-state
    
        junction = addJunction(chart, ...
            [state_dwellPos(1) + POS.W * 0.5, ...
                state_dwellPos(2) + POS.H + POS.J_H]);
    end
    
    function [ junction ] = addJunctionDwell2choose(state_dwellPos)
    % adds a junction connecting a dwell state and a choose state (backtracking)
    
        junction = addJunction(chart, ...
            [state_dwellPos(1) + POS.W * 0.9, ...
                state_dwellPos(2) - POS.H + POS.J_H]);
    end
    
    function [ junction ] = addJunctionTrans( baseX, baseY, iTrans )
        junction = addJunction(chart, [baseX, baseY + (iTrans * POS.J_H)]);
    end
    
    function [ initIdx ] = addTransitionInitial( loc, state_init, state_in, initIdx )
    % adds a transition connecting the initial state and an entry state
    % (if the location is initial)
    
        % get label from Java
        label = char(printer.getTransitionInitLabel(loc, initIdx));
        
        % the label is non-empty if and only if the location is initial
        if (~ isempty(label))
            initIdx = initIdx + 1;
            transition = ...
                addTransition(chart, state_init, state_in, label, 2, 11);
            transition.LabelPosition(1) = transition.DestinationEndPoint(1) + 5;
            transition.LabelPosition(2) = transition.DestinationEndPoint(2) - ...
                transition.LabelPosition(4) - 5;
        end
    end
    
    function addTransitionIn2choose( state_in, junction_in2dwell )
    % adds a transition 'entry state -> transition choosing junction'
    
        addTransition(chart, state_in, junction_in2dwell, '', 6, 0);
    end
    
    function addTransitionDwell2leave( state_dwell, junction_dwell2next )
    % add transition 'dwell state -> leave junction'
    % = dwelling successful
    
        label = char(printer.getTransitionDwell2leaveLabel());
        transition = addTransition(chart, state_dwell, ...
            junction_dwell2next, label, 6, 0);
        midPt = transition.MidPoint;
        transition.LabelPosition(1) = midPt(1) + 5;
        transition.LabelPosition(2) = midPt(2) - 5;
    end
    
    function addTransitionDwell2backtrack( state_dwell, junction_dwell2choose, loc, optEagerViolation )
    % adds a transition 'dwell state -> backtrack junction'
    % = invariant violation
    
        label = char(printer.getTransitionDwell2backtrackLabel(loc));
        transition = addTransition(chart, state_dwell, ...
            junction_dwell2choose, label, 1, 6);
        transition.MidPoint(1) = transition.MidPoint(1) - 10;
        transition.DestinationEndPoint(1) = ...
            transition.DestinationEndPoint(1) - 5;
        midPt = transition.MidPoint;
        transition.LabelPosition(1) = ...
            midPt(1) - transition.LabelPosition(3) - 5;
        transition.LabelPosition(2) = midPt(2) - 5;
        
        if (optEagerViolation)
            % execute this transition first if option is set accordingly
            transition.ExecutionOrder = 1;
        end
    end
    
    function addTransitionLeave2dwell( junction_dwell2next, state_dwell )
    % adds a transition 'leave junction -> dwell state'
    % = maximum simulation time passed: stop simulation
    
        label = char(printer.getTransitionLeave2dwellLabel());
        transition = addTransition(chart, junction_dwell2next, ...
            state_dwell, label, 9, 7);
        midPt = transition.MidPoint;
        transition.LabelPosition(1) = ...
            midPt(1) - transition.LabelPosition(3) - 5;
        transition.LabelPosition(2) = midPt(2) - 5;
    end
    
    function addTransitionChoose2dwell( state_choose, state_dwell )
    % adds a transition 'choose state -> dwell state'
    % = try the next time choice
    
        label = char(printer.getTransitionChoose2dwellLabel());
        transition = addTransition(chart, state_choose, state_dwell, ...
            label, 7, 11);
        midPt = transition.MidPoint;
        transition.LabelPosition(1) = ...
            midPt(1) - (transition.LabelPosition(3) / 2);
        transition.LabelPosition(2) = midPt(2) - 10;
    end
    
    function addTransitionChooseJ2choose( junction_in2dwell, state_choose )
    % adds a transition 'transition choose junction -> choose state'
    % = try the next (original) transition
    
        label = char(printer.getTransitionChooseJ2chooseLabel());
        transition = addTransition(chart, junction_in2dwell, ...
            state_choose, label, 6, 0);
        transition.MidPoint(1) = transition.MidPoint(1) + 10;
        transition.DestinationEndPoint(1) = ...
            transition.DestinationEndPoint(1) + 5;
        midPt = transition.MidPoint;
        transition.LabelPosition(1) = midPt(1) + 5;
        transition.LabelPosition(2) = midPt(2) - 25;
    end
    
    function addTransitionChoose2chooseJ( state_choose, junction_in2dwell )
    % adds a transition 'choose state -> transition choose junction'
    % = backtracking (to choose the next transition)
    
        label = char(printer.getTransitionChoose2chooseJLabel());
        transition = addTransition(chart, state_choose, ...
            junction_in2dwell, label, 0, 6);
        transition.MidPoint(1) = transition.MidPoint(1) - 10;
        transition.DestinationEndPoint(1) = ...
            transition.DestinationEndPoint(1) - 5;
        midPt = transition.MidPoint;
        transition.LabelPosition(1) = ...
            midPt(1) - transition.LabelPosition(3) - 5;
        transition.LabelPosition(2) = midPt(2) - 10;
    end
    
    function addTransitionChooseTime2dwell( junction_dwell2choose, state_choose )
    % adds a transition 'time choose junction -> dwell state'
    % = choose new dwelling time
    
        label = char(printer.getTransitionChooseTime2dwellLabel());
        transition = addTransition(chart, junction_dwell2choose, ...
            state_choose, label, 0, 5);
        midPt = transition.MidPoint;
        transition.LabelPosition(1) = midPt(1) + 5;
        transition.LabelPosition(2) = midPt(2) - 20;
    end
    
    function addTransitionInJ2dwell( junction_in2dwell, state_dwell )
    % adds a transition 'entry junction -> dwell state'
    % = no transitions are left
    
        label = char(printer.getTransitionInJ2dwellLabel());
        transition = addTransition(chart, junction_in2dwell, state_dwell, ...
            label, 9, 9);
        transition.DestinationEndPoint(1) = state_dwell.Position(1);
        transition.DestinationEndPoint(2) = ...
            state_dwell.Position(2) + (POS.H / 2);
        transition.SourceOClock = 9;
        transition.MidPoint(1) = transition.MidPoint(1) + 30;
        midPt = transition.MidPoint;
        transition.LabelPosition(1) = ...
            midPt(1) - transition.LabelPosition(3) - 5;
        transition.LabelPosition(2) = midPt(2) - 25;
    end
    
    function addTransitionBacktrack2dwell( junction_dwell2choose, state_dwell )
    % adds a transition 'backtrack junction -> dwell state'
    % = deadlock: stop simulation
    
        label = char(printer.getTransitionBacktrack2dwellLabel());
        transition = addTransition(chart, junction_dwell2choose, ...
            state_dwell, label, 6, 0);
        transition.MidPoint(1) = transition.MidPoint(1) + 10;
        transition.DestinationEndPoint(1) = ...
            transition.DestinationEndPoint(1) + 5;
        midPt = transition.MidPoint;
        transition.LabelPosition(1) = midPt(1) + 5;
        transition.LabelPosition(2) = midPt(2) - 10;
    end
    
    function addTransitionLeave2trans( junction_dwell2next, junction_trans, iTrans )
    % adds a transition 'leave junction -> transition junction'
    
        label = char(printer.getTransitionLeave2transLabel(iTrans));
        if (mod(iTrans, 2) == 0)
            % go right
            transition = addTransition(chart, junction_dwell2next, ...
                junction_trans, label, 3, 3);
            midPt = transition.MidPoint;
            transition.LabelPosition(1) = midPt(1) + 5;
        else
            % go left
            transition = addTransition(chart, junction_dwell2next, ...
                junction_trans, label, 9, 9);
            midPt = transition.MidPoint;
            transition.LabelPosition(1) = ...
                midPt(1) - transition.LabelPosition(3) - 5;
        end
        transition.LabelPosition(2) = midPt(2) - 5;
    end
    
    function addTransitionTrans2in( junction_trans, state_in, trans, juncX )
    % adds a transition 'transition junction -> entry state'
    % = original transition
    
        label = char(printer.getTransitionTrans2inLabel(trans));
        if (state_in.Position(1) > juncX)
            % go right
            transition = addTransition(chart, junction_trans, state_in, ...
                label, 3, 9);
            transition.DestinationOClock = 9;
            transition.SourceOClock = 3;
            transition.DestinationEndPoint(1) = state_in.Position(1);
        elseif (state_in.Position(1) + POS.W > juncX)
            % self-loop
            transition = addTransition(chart, junction_trans, state_in, ...
                label, 9, 9);
            transition.DestinationOClock = 9;
            transition.SourceOClock = 9;
            transition.DestinationEndPoint(1) = state_in.Position(1);
        else
            % go left
            transition = addTransition(chart, junction_trans, state_in, ...
                label, 9, 3);
            transition.DestinationOClock = 3;
            transition.SourceOClock = 9;
            transition.DestinationEndPoint(1) = state_in.Position(1) + POS.W;
        end
        transition.DestinationEndPoint(2) = POS.Y0 + (POS.H / 2);
        midPt = transition.MidPoint;
        transition.LabelPosition(1) = midPt(1) + 5;
        transition.LabelPosition(2) = midPt(2);
    end
    
    function addTransitionInit2in( state_init, numTransMax, initIdx )
    % constant initialization string
    % NOTE: This depends on the maximum number of outgoing transitions and the
    
        label = char(printer.getTransitionInit2inLabel(numTransMax, initIdx));
        transition = addTransition(chart, [], state_init, label, 6, 0);
        srcX = state_init.Position(1) + state_init.Position(3) / 2;
        transition.SourceEndPoint = [srcX, state_init.Position(2) - 20];
        transition.SourceOClock = 6;
        transition.LabelPosition(1) = srcX + 5;
        transition.LabelPosition(2) = ...
            transition.DestinationEndPoint(2) - transition.LabelPosition(4);
    end

% end of main function
end


function addAuxiliaryVariables( chart, printer, numTransMax )
% adds the auxiliary variables
% These are the variables not being part of the model, but used for controlling
% the simulation (like the dwelling time, backtracking, etc.).

    printer.initializeVariables(numTransMax);
    varIt = printer.variables.iterator();
    % add variables
    while (varIt.hasNext())
        var = varIt.next();
        sfVar = Stateflow.Data(chart);
        sfVar.Name = char(var.name);
        propIt = var.props.iterator();
        while (propIt.hasNext())
            prop = propIt.next();
            sfVar.setPropValue(char(prop.name), char(prop.value));
        end
    end
end


function addConstants( chart, constants, PREFIX_VARIABLE )
% adds constants and initializes them

    itConst = constants.entrySet().iterator();
    while (itConst.hasNext())
        constant = itConst.next();
        var = addVariable(chart, [PREFIX_VARIABLE, constant.getKey()], ...
            'Constant');
        assert(~ isempty(constant.getValue()), 'Constant not defined.');
        var.Props.InitialValue = num2str(constant.getValue());
    end
end


% --- functions for adding Stateflow components ---


function [ state ] = addState( chart, label, position )
% adds a state with a label and a size/position

    state = Stateflow.State(chart);
    state.LabelString = label;
    state.Position = position;
end


function [ junction ] = addJunction( chart, center )
% adds a junctions at a center position

    junction = Stateflow.Junction(chart);
    junction.Position.Center = center;
end


function [ transition ] = addTransition( chart, src, dest, label, srcO, dstO )
% adds a new transition with a label and a source/destination clock angle

    transition = Stateflow.Transition(chart);
    transition.Source = src;
    transition.Destination = dest;
    transition.LabelString = label;
    transition.SourceOClock = srcO;
    transition.DestinationOClock = dstO;
end


function [ var ] = addVariable( chart, name, scope, update )
% adds a variable
    var = Stateflow.Data(chart);
    var.Name = name;
    var.Scope = scope;
    if (exist('update', 'var'))
        var.Update = update;
    end
end


function addRandomBlock( printer, name, pos, minString, maxString )
% adds a random block

    add_block('dspsrcs4/Random Source', name, 'Position', pos, ...
        'SrcType', 'Uniform', 'SampMode', 'Continuous', 'MinVal', minString, ...
        'MaxVal', maxString, ...
        'RepMode', 'Specify seed', 'rawSeed', char(printer.V_seed.name));
end


function linkToScope( modelName, chartName, outPort, inPort, lineName )
% connects the chart with the scope wrt. given ports

    line = add_line(modelName, [chartName, '/', num2str(outPort)], ...
        ['Scope/', num2str(inPort)], 'autorouting', 'on');
    set_param(line, 'Name', lineName);
end