#include <list>
#include "determinizeTest.h"

#include <automaton/FSM/NFA.h>
#include <automaton/TA/NFTA.h>
#include <automaton/PDA/InputDrivenNPDA.h>
#include <automaton/PDA/InputDrivenDPDA.h>
#include <automaton/PDA/VisiblyPushdownNPDA.h>
#include <alphabet/BottomOfTheStackSymbol.h>

#include "automaton/determinize/Determinize.h"

CPPUNIT_TEST_SUITE_NAMED_REGISTRATION( determinizeTest, "automaton" );
CPPUNIT_TEST_SUITE_REGISTRATION( determinizeTest );

void determinizeTest::setUp() {
}

void determinizeTest::tearDown() {
}

void determinizeTest::testDeterminizeNFA() {
  automaton::NFA < > automaton(DefaultStateType(1));

  automaton.addState(DefaultStateType(1));
  automaton.addState(DefaultStateType(2));
  automaton.addState(DefaultStateType(3));
  automaton.addInputSymbol(DefaultSymbolType("a"));
  automaton.addInputSymbol(DefaultSymbolType("b"));

  automaton.addTransition(DefaultStateType(1), DefaultSymbolType("a"), DefaultStateType(2));
  automaton.addTransition(DefaultStateType(2), DefaultSymbolType("b"), DefaultStateType(1));

  automaton.addFinalState(DefaultStateType(3));

  automaton::DFA < DefaultSymbolType, std::set < DefaultStateType > > determinized = automaton::determinize::Determinize::determinize(automaton);

  CPPUNIT_ASSERT(determinized.getStates().size() == 3);

}

void determinizeTest::testDeterminizeIDPDA() {
  automaton::InputDrivenNPDA < > automaton(DefaultStateType(1), DefaultSymbolType('S'));

  automaton.addInputSymbol(DefaultSymbolType("a"));
  automaton.addInputSymbol(DefaultSymbolType("b"));

  automaton.setPushdownStoreOperation(DefaultSymbolType("a"), std::vector<DefaultSymbolType>{}, std::vector<DefaultSymbolType> {});
  automaton.setPushdownStoreOperation(DefaultSymbolType("b"), std::vector<DefaultSymbolType>{}, std::vector<DefaultSymbolType> {});

  automaton.addState(DefaultStateType(1));
  automaton.addState(DefaultStateType(2));
  automaton.addState(DefaultStateType(3));
  automaton.addTransition(DefaultStateType(1), DefaultSymbolType("a"), DefaultStateType(2));
  automaton.addTransition(DefaultStateType(2), DefaultSymbolType("b"), DefaultStateType(1));

  automaton.addFinalState(DefaultStateType(3));

  automaton::InputDrivenDPDA < > determinized = automaton::determinize::Determinize::determinize(automaton);

  CPPUNIT_ASSERT(determinized.getStates().size() == 3);
}

void determinizeTest::testDeterminizeVPA() {
  automaton::VisiblyPushdownNPDA < > automaton(DefaultSymbolType(alphabet::BottomOfTheStackSymbol {}));

  automaton.addCallInputSymbol(DefaultSymbolType('a'));
  automaton.addReturnInputSymbol(DefaultSymbolType('^'));

  automaton.addPushdownStoreSymbol(DefaultSymbolType('A'));
  automaton.addPushdownStoreSymbol(DefaultSymbolType('B'));
  automaton.addPushdownStoreSymbol(DefaultSymbolType('C'));
  automaton.addPushdownStoreSymbol(DefaultSymbolType('D'));
  automaton.addPushdownStoreSymbol(DefaultSymbolType('E'));
  automaton.addPushdownStoreSymbol(DefaultSymbolType('F'));
  automaton.addPushdownStoreSymbol(DefaultSymbolType('T'));

  automaton.addState(DefaultStateType(0));
  automaton.addState(DefaultStateType(1));
  automaton.addState(DefaultStateType(2));
  automaton.addState(DefaultStateType(3));
  automaton.addState(DefaultStateType(4));
  automaton.addState(DefaultStateType(5));
  automaton.addState(DefaultStateType(6));


  automaton.addCallTransition(DefaultStateType(0), DefaultSymbolType('a'), DefaultStateType(0), DefaultSymbolType('A'));
  automaton.addReturnTransition(DefaultStateType(0), DefaultSymbolType('^'), DefaultSymbolType('A'), DefaultStateType(0));

  automaton.addCallTransition(DefaultStateType(0), DefaultSymbolType('a'), DefaultStateType(1), DefaultSymbolType('B'));

  automaton.addCallTransition(DefaultStateType(1), DefaultSymbolType('a'), DefaultStateType(2), DefaultSymbolType('C'));
  automaton.addCallTransition(DefaultStateType(2), DefaultSymbolType('a'), DefaultStateType(2), DefaultSymbolType('D'));
  automaton.addReturnTransition(DefaultStateType(2), DefaultSymbolType('^'), DefaultSymbolType('D'), DefaultStateType(2));
  automaton.addReturnTransition(DefaultStateType(2), DefaultSymbolType('^'), DefaultSymbolType('C'), DefaultStateType(3));

  automaton.addCallTransition(DefaultStateType(3), DefaultSymbolType('a'), DefaultStateType(4), DefaultSymbolType('E'));
  automaton.addCallTransition(DefaultStateType(4), DefaultSymbolType('a'), DefaultStateType(4), DefaultSymbolType('F'));
  automaton.addReturnTransition(DefaultStateType(4), DefaultSymbolType('^'), DefaultSymbolType('F'), DefaultStateType(4));
  automaton.addReturnTransition(DefaultStateType(4), DefaultSymbolType('^'), DefaultSymbolType('E'), DefaultStateType(5));

  automaton.addReturnTransition(DefaultStateType(5), DefaultSymbolType('^'), DefaultSymbolType('B'), DefaultStateType(6));

  automaton.addInitialState(DefaultStateType(0));
  automaton.addFinalState(DefaultStateType(4));
}

void determinizeTest::testDeterminizeNFTA() {
  automaton::NFTA < > automaton;

  const std::ranked_symbol < > a ('a', 2);
  const std::ranked_symbol < > b ('b', 1);
  const std::ranked_symbol < > c ('c', 0);
  const std::set<std::ranked_symbol < > > alphabet {a, b, c};
  automaton.setInputAlphabet(alphabet);

  automaton.addState(DefaultStateType(1));
  automaton.addState(DefaultStateType(2));
  automaton.addState(DefaultStateType(3));

  std::vector<DefaultStateType> a1States = {DefaultStateType(1), DefaultStateType(3)};
  automaton.addTransition(a, a1States, DefaultStateType(1));
  automaton.addTransition(a, a1States, DefaultStateType(3));
  std::vector<DefaultStateType> a2States = {DefaultStateType(3), DefaultStateType(3)};
  automaton.addTransition(a, a2States, DefaultStateType(2));
  std::vector<DefaultStateType> bStates = {DefaultStateType(2)};
  automaton.addTransition(b, bStates, DefaultStateType(1));
  std::vector<DefaultStateType> cStates;
  automaton.addTransition(c, cStates, DefaultStateType(3));

  automaton.addFinalState(DefaultStateType(3));


  automaton::DFTA < > determinized = automaton::determinize::Determinize::determinize(automaton);

  CPPUNIT_ASSERT(determinized.getStates().size() == 5);
  CPPUNIT_ASSERT(determinized.getFinalStates().size() == 3);
  CPPUNIT_ASSERT(determinized.getTransitions().size() == 15);
}