indexing
	description: "Non-deterministic finite state automata"
	status: "See notice at end of class"
	date: "$Date$"
	revision: "$Revision$"

deferred class interface
	NDFA

feature -- Access

	dfa: FIXED_DFA
			-- DFA built by routine construct_dfa,
			-- which recognizes the same language.

	find_e_successors (source: INTEGER): LINKED_LIST [INTEGER]
			-- Epsilon successors of source.
			-- Void if no successor.
		require
			source_in_automaton: source >= 1 and source <= nb_states

	find_successors (source, input_doc: INTEGER): LINKED_LIST [INTEGER]
			-- Successors of source on input_doc;
			-- Void if no successor
		require
			source_in_automaton: source >= 1 and source <= nb_states
			possible_input_doc: input_doc >= 0 and input_doc <= greatest_input

	greatest_input: INTEGER
			-- Greatest input used for the transitions from state
			-- to state (the smallest one is zero)
			-- (from AUTOMATON)

	start_number: INTEGER
			-- Unique start state used for the beginning of
			-- the automaton's operation
			-- (from AUTOMATON)
	
feature -- Measurement

	nb_states: INTEGER
			-- Number of states in the automaton
			-- (from AUTOMATON)
	
feature -- Status setting

	set_final (state, f: INTEGER)
			-- Make state final for regular expression f.
			-- (from AUTOMATON)

	set_start (n: INTEGER)
			-- Select state n as the starting state.
			-- (from AUTOMATON)
		require -- from AUTOMATON
			no_other_start: start_number = 0 or start_number = n
			is_in_automaton: n <= nb_states and n >= 1

	set_state
			-- Make a new state.
			-- (from AUTOMATON)
	
feature -- Element change

	set_e_transition (source, target: INTEGER)
			-- Set epsilon transition from source to target.
		require
			source_in_automaton: source >= 1 and source <= nb_states
			target_in_automaton: target >= 1 and target <= nb_states

	set_transition (source, input_doc, target: INTEGER)
			-- Set transition from source to target for input_doc.
		require -- from  AUTOMATON
			True
		require else
			source_in_automaton: source >= 1 and source <= nb_states
			target_in_automaton: target >= 1 and target <= nb_states
			possible_input_doc: input_doc >= 0 and input_doc <= greatest_input
	
feature -- Removal

	delete_transition (source, input_doc, target: INTEGER)
			-- Delete transition from source to target on input_doc.
		require
			source_in_automaton: source >= 1 and source <= nb_states
			target_in_automaton: target >= 1 and target <= nb_states
			possible_input_doc: input_doc >= 0 and input_doc <= greatest_input
	
feature -- Transformation

	construct_dfa
			-- Create an equivalent deterministic finite automaton.
		require
			start_number_designated: start_number > 0
	
invariant

		-- from ANY
	reflexive_equality: standard_is_equal (Current)
	reflexive_conformance: conforms_to (Current)

end -- class NDFA