22 std::cout <<
"NTA:\n";
30 std::cout <<
"DTA:\n";
48 alphabet.insert(succs.begin(), succs.end());
72 std::cout <<
"Adding path: ";
75 for(
const auto &step : path)
80 std::cout <<
", " << l->location_number <<
':' 81 << l->source_location.as_string();
99 std::cout <<
"Final state: " << state <<
'\n';
113 std::cout <<
"Determinising automaton with " <<
nta.
num_states 128 std::cout <<
"There are " << init_states.size() <<
" init states\n";
146 for(alphabett::iterator it=
alphabet.begin();
168 std::cout <<
"Produced DTA with " <<
dta.
num_states <<
" states and " 185 std::vector<statet> queue(states.size());
188 for(state_sett::iterator it=states.begin();
192 queue.push_back(*it);
196 while(!queue.empty())
198 statet state=queue.back();
206 for(state_sett::iterator it=next_states.begin();
207 it!=next_states.end();
210 if(states.find(*it)==states.end())
214 queue.push_back(*it);
240 for(state_sett::iterator it=s.begin();
247 std::cout <<
"NTA state " << *it
248 <<
" is accepting, so accepting DTA state " 249 << state_num <<
'\n';
262 state_mapt::iterator it=
dstates.find(s);
280 transitions.push_back(trans);
290 assert(s < transitions.size());
293 trans.insert(std::make_pair(a, t));
315 assert(s < transitions.size());
321 for(transitionst::iterator it=range.first;
325 t.insert(it->second);
334 for(
const auto &state : s)
342 for(std::size_t i=0; i < dtrans.size(); ++i)
346 for(
const auto &trans : dta_transitions)
349 unsigned int j=trans.second;
353 transitions.insert(std::make_pair(l, state_pair));
363 old_table.swap(transitions);
365 for(std::size_t i=0; i < old_table.size(); i++)
383 new_init=add_state();
386 add_trans(new_init, epsilon, s);
389 std::cout <<
"Reversing automaton, old init=" <<
init_state 390 <<
", new init=" << new_init <<
", old accept=" 399 for(std::size_t i=0; i < old_table.size(); i++)
403 for(
const auto &t : trans)
406 unsigned int j=t.second;
427 for(
const auto &s : new_states)
431 for(
const auto &t : trans)
433 unsigned int j=t.second;
435 if(reachable.find(j)==reachable.end())
443 tmp.swap(new_states);
445 while(!new_states.empty());
449 if(reachable.find(i)==reachable.end())
472 str <<
"Accept states: ";
479 for(
unsigned int i=0; i < transitions.size(); ++i)
481 for(
const auto &trans : transitions[i])
486 str << i <<
" -- " << l->location_number <<
" --> " << j <<
'\n';
495 for(
const auto &trans : transitions)
void get_transitions(sym_mapt &transitions)
void epsilon_closure(state_sett &s)
std::pair< transitionst::iterator, transitionst::iterator > transition_ranget
std::multimap< goto_programt::targett, statet > transitionst
bool in_alphabet(goto_programt::targett t)
std::vector< transitionst > transition_tablet
statet find_dstate(state_sett &s)
void swap(automatont &that)
void accept_states(state_sett &states)
std::pair< statet, statet > state_pairt
static const statet no_state
void pop_unmarked_dstate(state_sett &s)
std::list< Target > get_successors(Target target) const
statet add_dstate(state_sett &s)
void add_trans(statet s, goto_programt::targett a, statet t)
void add_dtrans(state_sett &s, goto_programt::targett a, state_sett &t)
bool is_accepting(statet s)
std::list< path_nodet > patht
std::size_t count_transitions()
void build_alphabet(goto_programt &program)
void add_path(patht &path)
std::set< statet > state_sett
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
std::vector< state_sett > unmarked_dstates
std::multimap< goto_programt::targett, state_pairt > sym_mapt
void reverse(goto_programt::targett epsilon)
void move(statet s, goto_programt::targett a, state_sett &t)
transition_tablet transitions
#define Forall_goto_program_instructions(it, program)
goto_programt::targett epsilon
void output(std::ostream &str)
void set_accepting(statet s)
instructionst::iterator targett