classdef LTLAutomata < handle
% Reads a Rabin autonomata file generated using the --output=automaton in
% ltldstar.
% Example:
%   echo 'G i s U s a' > stop_sign.ltl
%   ltl2dstar --ltl2nba=spin:ltl2ba --stutter=yes --output=automaton stop_sign.ltl stop_sign.aut
% Steps through the Automata based on XXX
    
    properties
        num_states = 0
        num_ap = 0
        state_index_to_id
        transition_map
        start_state_index
        ap_names
        cur_state_index
        fail_state_indices
        
        internal_proposition_state_out
    end
    
    methods
        function obj = LTLAutomata(aut_file)
            obj.read(aut_file)
            obj.cur_state_index = obj.start_state_index;
        end
        
        function good_run = check_run(obj, ts, xs, us, traj2propFunc, run_start_state_index, internal_proposition_state_in)

            if nargin >= 6
                obj.cur_state_index = run_start_state_index;
            else
                obj.cur_state_index = obj.start_state_index;
            end
            
            if nargin >= 7
                [propositions_run, ap_names, obj.internal_proposition_state_out] = traj2propFunc(ts, xs, us, internal_proposition_state_in);
            else
                [propositions_run, ap_names] = traj2propFunc(ts, xs, us);
            end
            
            
            %TODO move columns of propositions around to match ap_names
            %to obj.ap_names
            
            for i = 1:length(propositions_run)
                obj.step(propositions_run(i,:));
                
                if ismember(obj.cur_state_index, obj.fail_state_indices)
                    good_run = false;
                    return
                end
                
            end
            good_run = true;
        end
        
        function index = state_id_to_index(obj, id)
            index = find(obj.state_index_to_id == id, 1);
        end
        
        function step(obj, propositions)
        % updates the cur_state to the next state based on the propostions.
        % propositions are a list of 0 and 1 for corresponding to obj.ap.
        
            to_transition_index = obj.binary2Decimal(fliplr(propositions)) + 1;
            obj.cur_state_index = obj.transition_map(obj.cur_state_index, to_transition_index);
        end
        
        function dec = binary2Decimal(~, bi)
            base2 = 2.^(length(bi)-1:-1:0);
            dec = dot(base2,bi);
        end
        
        function read(obj, aut_file)
            if ~exist(aut_file, 'file')
                return
            end
            file_id = fopen(aut_file);
            data = fread(file_id, '*char')';
            fclose(file_id);
            data = regexp(data, {'\n'}, 'split');
            data_lines = regexp(data{1}, ':', 'split');
            num_lines = length(data{1});
            
            % read front information
            i = 1;
            while i < num_lines
                switch data_lines{i}{1}
                    case 'States'
                        obj.num_states = str2double(data_lines{i}{2});
                    case 'Acceptance-Pairs'
                        
                    case 'Start'
                        start_state = str2double(data_lines{i}{2});
                    case 'AP'
                        line_split = regexp(data_lines{i}{2},'"','split');
                        obj.num_ap = str2double(line_split{1});
                        for k = 1:obj.num_ap
                            obj.ap_names{k} = line_split{2*k};
                        end
                    case '---'
                        break
                end
                i = i + 1;
            end
            assert(obj.num_states > 0 && obj.num_ap > 0, 'Bad automata file -- num_states read %d, num_ap %d', obj.num_states, obj.num_ap);
            
            % read state information
            state_line_init = i + 1;
            state_line = state_line_init;
            obj.state_index_to_id = zeros(1, obj.num_states);
            for i = 1:obj.num_states
                assert(strcmp(data_lines{state_line}{1},'State') && state_line < num_lines, 'Bad automata file');
                state_id = str2double(data_lines{state_line}{2});
                obj.state_index_to_id(i) = state_id;
                if strcmp(strtrim(data_lines{state_line+1}{2}), '-0')
                    obj.fail_state_indices = [obj.fail_state_indices, i];
                end
                state_line = state_line + 2^obj.num_ap + 2;
            end
            obj.start_state_index = obj.state_id_to_index(start_state);
            
            % read transition information
            state_line = state_line_init;
            obj.transition_map = zeros(obj.num_states, 2^obj.num_ap);
            for i = 1:obj.num_states
                for k = 1:2^obj.num_ap
                    to_state = str2double(data_lines{state_line+k+1}{1});
                    obj.transition_map(i,k) = obj.state_id_to_index(to_state);
                end
                state_line = state_line + 2^obj.num_ap + 2;
            end
            
        end
    end
end