/*
 * nfasim.pro
 *
 * Simulation and Conversion of an NFA (using Prolog)
 *
 * Robert Keller
 * 6 April 2009
 *
 * This is purely for demonstration purposes, not for generality or efficiency.
 * A fixed NFA, as defined by trans, initial, and accepting, is simulated.
 * The same NFA is converted to a DFA using the subset algorithm.
 *
 * Running: 
 *    % swipl -f nfasim.pro
 *    ?- test.
 */

/*
 * NFA Example
 */

/*
 * trans(State, Symbol, NewState) defines ordinary transitions
 *
 * trans(State, NewState) defines spontaneous transitions (epsilon transitions)
 */


trans(c, d).
trans(b, e).
trans(a, 0, a).
trans(a, 1, b).
trans(a, 1, c).
trans(d, 0, d).
trans(e, 1, e).
trans(e, 1, a).

/*
 * initial defines initial states
 */

initial(a).
initial(c).

/*
 * accepting defines accepting states
 */

accepting(d).
accepting(e).


/*
 * accepted(InputSequence) succeeds on any accepted sequence.
 */

accepted(InputSequence) :-
    simulate(InputSequence, StateSetSequence),
    last(StateSetSequence, Last),
    setof1(State, accepting(State), Accepting),
    intersects(Last, Accepting).


/*
 * simulate(InputSequence, StateSetSequence) gives the sequence of sets of states
 * corresponding to InputSequence, when started on the set of initial states.
 */

simulate(InputSequence, StateSetSequence) :-
    setof1(Q, initial(Q), Initial),
    simulate(InputSequence, Initial, StateSetSequence).

/*
 * simulate(InputSequence, StateSet, StateSetSequence) simulates the NFA
 * on an input sequence when started in one of an arbitrary set of states.
 */

/* For the empty input sequence, we just get the closure of the state set. */

simulate([], StateSet, [StateSet2]) :- closure(StateSet, StateSet2).

/* For a non-empty input sequence, we start with the first symbol, and continue on. */

simulate([A | X], StateSet, [StateSet2 | StateSetSequence]) :-
    closure(StateSet, StateSet2),
    oneStep(StateSet2, A, NewStateSet),
    simulate(X, NewStateSet, StateSetSequence).


/* 
 * oneStep(StateSet, Symbol, NewStateSet) gives the new states resulting from
 * assimilating a single input symbol.
 */

oneStep(StateSet, Symbol, Closure) :-
    setof1(NewState, State^(trans(State, Symbol, NewState), member(State, StateSet)), NewStateSet),
    closure(NewStateSet, Closure).


/*
 * closure(R, S) means that S is the set of states spontaneously reachable
 * from states in R.
 */
closure(R, S) :-
    closure(R, R, S).

/*
 * closure(Acc, Recent, Result) is an auxiliary predicate for computing closure(R, S).
 * Acc represents the set of accumulated reachable states,
 * Recent is the set of states most recently added, and
 * Result is the end result.
 * 
 */

closure(Acc, Recent, Result) :-
    (
    setof1(Q, P^(member(P, Recent), trans(P, Q)), Next),
    setDifference(Next, Acc, New)
    ),
    (
    New = [] 
        -> Result = Acc				% no new additions
        ;    (
            setUnion(Acc, New, Union),		% Accumulate the new additions.
            closure(Union, New, Result)	% Recurse with the new accumulation.
             )
    ).


/*
 * setof1(Form, Goal, Result) gives as Result the set of (as a list)
 * Form that satisfy Goal. It differs from setof in that it does not fail
 * if the result is empty.
 */

setof1(Form, Goal, Result) :- setof(Form, Goal, Result) -> true ; Result = [].


/*
 * setDifference(R, S, Diff) means that Diff is the set difference of R minus S, i.e.
 * Diff contains the elements of R that are not in S.
 */

setDifference(R, S, Diff) :-
    setof1(X, (member(X, R), \+member(X, S)), Diff).

/* 
 * setUnion(R, S, Union) means that Union is the set union of R with S, i.e.
 * Union contains the elements of R together with those of S.
 */

setUnion(R, S, Union) :-
    setof1(X, (member(X, R); member(X, S)), Union).


/* 
 * intersects(R, S) succeeds if there is an element common to both R and S.
 */

intersects(R, S) :-
    member(X, R), member(X, S).


/*
 * Sequence generator, for testing.
 * gen(Alphabet, MaxLength, Sequence) generates all sequences over Alphabet 
 * up to MaxLength long, in lexicographic order.
 */

gen(_Alphabet, 0, []).

gen(Alphabet, Length, Sequence) :-
    Length > 0,
    Length1 is Length - 1,
    gen(Alphabet, Length1, Sequence).
    
gen(Alphabet, Length, [Letter | Sequence]) :-
    Length > 0,
    Length1 is Length - 1,
    member(Letter, Alphabet),
    gen(Alphabet, Length1, Sequence),
    length(Sequence, Length1).	% hack to avoid duplicates, could be improved.
    

/*
 * Testing predicate
 */

testAccepted(InputSequence) :-
    write('Input sequence '),
    write(InputSequence),
    (
    accepted(InputSequence)
        -> write(' is accepted.')
        ;    write(' is not accepted.')
    ),
    nl,
    write('The state-set sequence is '),
    simulate(InputSequence, StateSetSequence),
    write(StateSetSequence),
    write('.'),
    nl,
    nl.


/* Test cases */

test:-
    gen([0, 1], 5, Sequence),
    testAccepted(Sequence),
    fail.
test.


/**
 * NFA to DFA conversion
 * A fixed NFA, as defined by trans, initial, and accepting, is converted, then printed.
 */

makeDFA :-
    setof1(Q, initial(Q), Initial),
    closure(Initial, Closure),
    write(initial(Closure)), write('.'), nl, nl,
    makeDFAtransitions([Closure], [Closure], [], [0, 1], DFAtransitions),
    writeOnePerLine(DFAtransitions), nl.

makeDFAtransitions([], States, Acc, _Alphabet, Acc) :-
    setof1(State, accepting(State), Accepting),
    setof1(accepting(State), (member(State, States), intersects(State, Accepting)), Final),
    writeOnePerLine(Final), nl.

makeDFAtransitions([Set | Sets], Processed, Acc, Alphabet, Result) :-
    setof1(trans(Set, Symbol, NewSet), (member(Symbol, Alphabet), oneStep(Set, Symbol, NewSet)), Trans),
    setof1(NextState, (member(trans(_, _, NextState), Trans), \+member(NextState, Processed)), NewStates),
    append(NewStates, Processed, NewProcessed),
    append(NewStates, Sets, NewSets),
    append(Acc, Trans, NewAcc),
    makeDFAtransitions(NewSets, NewProcessed, NewAcc, Alphabet, Result).

writeOnePerLine([]).

writeOnePerLine([Trans | More]) :-
    write(Trans),
    write('.'),
    nl,
    writeOnePerLine(More).


/*
 * Sample output for simulation:
 *

Input sequence [] is accepted.
The state-set sequence is [[a, c, d]].

Input sequence [0] is accepted.
The state-set sequence is [[a, c, d], [a, d]].

Input sequence [1] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e]].

Input sequence [0, 0] is accepted.
The state-set sequence is [[a, c, d], [a, d], [a, d]].

Input sequence [0, 1] is accepted.
The state-set sequence is [[a, c, d], [a, d], [b, c, d, e]].

Input sequence [1, 0] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [d]].

Input sequence [1, 1] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [a, e]].

Input sequence [0, 0, 0] is accepted.
The state-set sequence is [[a, c, d], [a, d], [a, d], [a, d]].

Input sequence [0, 0, 1] is accepted.
The state-set sequence is [[a, c, d], [a, d], [a, d], [b, c, d, e]].

Input sequence [0, 1, 0] is accepted.
The state-set sequence is [[a, c, d], [a, d], [b, c, d, e], [d]].

Input sequence [0, 1, 1] is accepted.
The state-set sequence is [[a, c, d], [a, d], [b, c, d, e], [a, e]].

Input sequence [1, 0, 0] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [d], [d]].

Input sequence [1, 0, 1] is not accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [d], []].

Input sequence [1, 1, 0] is not accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [a, e], [a]].

Input sequence [1, 1, 1] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [a, e], [a, b, c, d, e]].

Input sequence [0, 0, 0, 0] is accepted.
The state-set sequence is [[a, c, d], [a, d], [a, d], [a, d], [a, d]].

Input sequence [0, 0, 0, 1] is accepted.
The state-set sequence is [[a, c, d], [a, d], [a, d], [a, d], [b, c, d, e]].

Input sequence [0, 0, 1, 0] is accepted.
The state-set sequence is [[a, c, d], [a, d], [a, d], [b, c, d, e], [d]].

Input sequence [0, 0, 1, 1] is accepted.
The state-set sequence is [[a, c, d], [a, d], [a, d], [b, c, d, e], [a, e]].

Input sequence [0, 1, 0, 0] is accepted.
The state-set sequence is [[a, c, d], [a, d], [b, c, d, e], [d], [d]].

Input sequence [0, 1, 0, 1] is not accepted.
The state-set sequence is [[a, c, d], [a, d], [b, c, d, e], [d], []].

Input sequence [0, 1, 1, 0] is not accepted.
The state-set sequence is [[a, c, d], [a, d], [b, c, d, e], [a, e], [a]].

Input sequence [0, 1, 1, 1] is accepted.
The state-set sequence is [[a, c, d], [a, d], [b, c, d, e], [a, e], [a, b, c, d, e]].

Input sequence [1, 0, 0, 0] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [d], [d], [d]].

Input sequence [1, 0, 0, 1] is not accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [d], [d], []].

Input sequence [1, 0, 1, 0] is not accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [d], [], []].

Input sequence [1, 0, 1, 1] is not accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [d], [], []].

Input sequence [1, 1, 0, 0] is not accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [a, e], [a], [a]].

Input sequence [1, 1, 0, 1] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [a, e], [a], [b, c, d, e]].

Input sequence [1, 1, 1, 0] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [a, e], [a, b, c, d, e], [a, d]].

Input sequence [1, 1, 1, 1] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [a, e], [a, b, c, d, e], [a, b, c, d, e]].

Input sequence [0, 0, 0, 0, 0] is accepted.
The state-set sequence is [[a, c, d], [a, d], [a, d], [a, d], [a, d], [a, d]].

Input sequence [0, 0, 0, 0, 1] is accepted.
The state-set sequence is [[a, c, d], [a, d], [a, d], [a, d], [a, d], [b, c, d, e]].

Input sequence [0, 0, 0, 1, 0] is accepted.
The state-set sequence is [[a, c, d], [a, d], [a, d], [a, d], [b, c, d, e], [d]].

Input sequence [0, 0, 0, 1, 1] is accepted.
The state-set sequence is [[a, c, d], [a, d], [a, d], [a, d], [b, c, d, e], [a, e]].

Input sequence [0, 0, 1, 0, 0] is accepted.
The state-set sequence is [[a, c, d], [a, d], [a, d], [b, c, d, e], [d], [d]].

Input sequence [0, 0, 1, 0, 1] is not accepted.
The state-set sequence is [[a, c, d], [a, d], [a, d], [b, c, d, e], [d], []].

Input sequence [0, 0, 1, 1, 0] is not accepted.
The state-set sequence is [[a, c, d], [a, d], [a, d], [b, c, d, e], [a, e], [a]].

Input sequence [0, 0, 1, 1, 1] is accepted.
The state-set sequence is [[a, c, d], [a, d], [a, d], [b, c, d, e], [a, e], [a, b, c, d, e]].

Input sequence [0, 1, 0, 0, 0] is accepted.
The state-set sequence is [[a, c, d], [a, d], [b, c, d, e], [d], [d], [d]].

Input sequence [0, 1, 0, 0, 1] is not accepted.
The state-set sequence is [[a, c, d], [a, d], [b, c, d, e], [d], [d], []].

Input sequence [0, 1, 0, 1, 0] is not accepted.
The state-set sequence is [[a, c, d], [a, d], [b, c, d, e], [d], [], []].

Input sequence [0, 1, 0, 1, 1] is not accepted.
The state-set sequence is [[a, c, d], [a, d], [b, c, d, e], [d], [], []].

Input sequence [0, 1, 1, 0, 0] is not accepted.
The state-set sequence is [[a, c, d], [a, d], [b, c, d, e], [a, e], [a], [a]].

Input sequence [0, 1, 1, 0, 1] is accepted.
The state-set sequence is [[a, c, d], [a, d], [b, c, d, e], [a, e], [a], [b, c, d, e]].

Input sequence [0, 1, 1, 1, 0] is accepted.
The state-set sequence is [[a, c, d], [a, d], [b, c, d, e], [a, e], [a, b, c, d, e], [a, d]].

Input sequence [0, 1, 1, 1, 1] is accepted.
The state-set sequence is [[a, c, d], [a, d], [b, c, d, e], [a, e], [a, b, c, d, e], [a, b, c, d, e]].

Input sequence [1, 0, 0, 0, 0] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [d], [d], [d], [d]].

Input sequence [1, 0, 0, 0, 1] is not accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [d], [d], [d], []].

Input sequence [1, 0, 0, 1, 0] is not accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [d], [d], [], []].

Input sequence [1, 0, 0, 1, 1] is not accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [d], [d], [], []].

Input sequence [1, 0, 1, 0, 0] is not accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [d], [], [], []].

Input sequence [1, 0, 1, 0, 1] is not accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [d], [], [], []].

Input sequence [1, 0, 1, 1, 0] is not accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [d], [], [], []].

Input sequence [1, 0, 1, 1, 1] is not accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [d], [], [], []].

Input sequence [1, 1, 0, 0, 0] is not accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [a, e], [a], [a], [a]].

Input sequence [1, 1, 0, 0, 1] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [a, e], [a], [a], [b, c, d, e]].

Input sequence [1, 1, 0, 1, 0] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [a, e], [a], [b, c, d, e], [d]].

Input sequence [1, 1, 0, 1, 1] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [a, e], [a], [b, c, d, e], [a, e]].

Input sequence [1, 1, 1, 0, 0] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [a, e], [a, b, c, d, e], [a, d], [a, d]].

Input sequence [1, 1, 1, 0, 1] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [a, e], [a, b, c, d, e], [a, d], [b, c, d, e]].

Input sequence [1, 1, 1, 1, 0] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [a, e], [a, b, c, d, e], [a, b, c, d, e], [a, d]].

Input sequence [1, 1, 1, 1, 1] is accepted.
The state-set sequence is [[a, c, d], [b, c, d, e], [a, e], [a, b, c, d, e], [a, b, c, d, e], [a, b, c, d, e]].

 *
 * Sample output for conversion:
 *

?- makeDFA.

initial([a, c, d]).

accepting([a, c, d]).
accepting([a, d]).
accepting([b, c, d, e]).
accepting([d]).

trans([a, c, d], 0, [a, d]).
trans([a, c, d], 1, [b, c, d, e]).
trans([a, d], 0, [a, d]).
trans([a, d], 1, [b, c, d, e]).
trans([b, c, d, e], 0, [d]).
trans([b, c, d, e], 1, [a, e]).
trans([d], 0, [d]).
trans([d], 1, []).
trans([], 0, []).
trans([], 1, []).

 *
 */