% file:    nfa.pl
% author:  Robert Keller
% purpose: convert non-deterministic finite-state acceptor into 
%          a deterministic finite-state acceptor.  This version allows
%          free transitions.
% $Id: nfa.pl,v 1.2 2001/12/05 05:13:29 keller Exp $

% setof1 is like setof, except that it never fails.
% If there is no member with the indicated property, then setof1 returns []
% whereas setof would fail in that case.

setof1(S, T, U) :- setof(S, T, U) -> true ; U = [].


% A machine is constructed, or deconstructed, from three things:
%
%    a list of transitions, where each transition has a form described below.
%
%    a set of starting states.  For a deterministic machine, this will be
%        a singleton.
%
%    a set of accepting states.
%
% (We use a functor to implement this composition, although we could convert
% it to a list if functors are to be avoided.)
%
% Our representation is machine(Starting, Transitions, Accepting).
%
% A transition has one of the following two forms:
%
%    [State, Symbol, NextState]
%
%    [State, NextState] indicating a "free" transition from State to NextState


% hasTransitions means that Machine has the indicated set of Transitions.

hasTransitions(machine(_Starting, Transitions, _Accepting), Transitions).


% hasStarting means that Machine has the indicated set of starting states.

hasStarting(machine(Starting, _Transitions, _Accepting), Starting).


% hasAccepting means that Machine has the indicated set of starting states.

hasAccepting(machine(_Starting, _Transitions, Accepting), Accepting).


% hasStates means that Machine has the state set States, as determined by
% its transitions.

hasStates(Machine, States) :- 
    setof1(State, hasState(Machine, State), States).


% hasState meanas that Machine has a state State.

hasState(Machine, State)   :- hasTransition(Machine, [State, _, _]).
hasState(Machine, State)   :- hasTransition(Machine, [_, _, State]).
hasState(Machine, State)   :- hasTransition(Machine, [State, _]).
hasState(Machine, State)   :- hasTransition(Machine, [_, State]).


% hasSymbol means that Machine has a symbol Symbol.

hasSymbol(Machine, Symbol) :- hasTransition(Machine, [_, Symbol, _]).


% hasTransition means that Machine has a Transition.

hasTransition(Machine, Transition) :- 
    hasTransitions(Machine, Transitions), 
    member(Transition, Transitions).


% hasSymbols means the machine has the indicated set of symbols.

hasSymbols(Machine, Symbols) :- 
    setof1(Symbol, hasSymbol(Machine, Symbol), Symbols).


% convert converts a non-deterministic machine into a determinisitc one.

convert(NonDeterministic, Deterministic) :-

    % The one starting state of the deterministic machine is the set of
    % starting states of the non-deterministic one.

    hasStarting(NonDeterministic, Nstarting),
    extensions(Nstarting, NonDeterministic, Dstarting),
    hasStarting(Deterministic, [Dstarting]),


    % The states of the deterministic machine are the reachable sets of
    % the non-deterministic machine.

    reachable(NonDeterministic, Dstates),

    
    % The accepting states are those states that contain an accepting state
    % of the non-deterministic machine.

    hasAccepting(NonDeterministic, Naccepting),
    containAccepting(Dstates, Naccepting, Daccepting),
    hasAccepting(Deterministic, Daccepting),

    hasSymbols(NonDeterministic, Symbols),
    

    % The transitions of the deterministic machine are formed as follows:
    % For a state of Dstates of the deterministic machine, which is actually
    % a set of states of the non-deterministic machine, consider collectively
    % the set Dstate2 of of states of the non-deterministic machine that are
    % targets of some state Dstate within Dstates for the given symbol.
    % A transition in the deterministic machine goes from Dstate with Symbol
    % to Dstate2.

    setof([Dstate, Symbol, Dstate2], 
          (member(Symbol, Symbols),
           member(Dstate, Dstates),
           targets(Dstate, Symbol, NonDeterministic, Dstate2)
           ),
          Dtransitions),

    hasTransitions(Deterministic, Dtransitions).


% containAccepting indicates those sets in Sos (set-of-states) that contain
% an accepting state.

containAccepting(Sos, Accepting, Contain) :-
    setof(S, (member(S, Sos), Q^(member(Q, S),member(Q, Accepting))), Contain).


% targets gives the set of next states S2 for the non-deterministic machine,
% given a current set S1 and a symbol.

targets(S1, Symbol, Machine, S2) :-
    setof1(Q2,
           Q1^(member(Q1, S1), 
               hasTransition(Machine, [Q1, Symbol, Q2])),
           S3),
    extensions(S3, machine, S2).


% extensions is the set of all states reachable from a state in S1 by
% zero or more free transitions.

extensions(S1, Machine, S2) :-
    extensionWave(S1, Machine, S3),
    (S1 == S3 -> S2 = S3 ; extensions(S3, Machine, S2)).


% extensionWave gives the set of states S2 for a non-deterministic machine,
% that are reachable by one free transition from a current set S1.

extensionWave(S1, Machine, S2) :-
    setof1(Q2,
           Q1^(member(Q1, S1), 
               hasTransition(Machine, [Q1, Q2])),
           S3),
    union(S1, S3, S2).


% reachable/2 determines the set of reachable states for the deterministic
% machine corresponding to the given non-deterministic one.

reachable(Machine, Reachable) :-
    hasStarting(Machine, Starting),
    extensions(Starting, Machine, EffectiveStarting),
    reachable([EffectiveStarting], Machine, Reachable).


% reachable/3 determines the set of states Sos2 for the deterministic
% machine that are reachable from Sos1, given the non-deterministic machine.

reachable(Sos1, Machine, Sos2) :-
    wave(Sos1, Machine, Sos3),
    (Sos1 == Sos3 -> Sos2 = Sos3 ; reachable(Sos3, Machine, Sos2)).


% wave determines the set of next state sets given a set of current next
% state sets.  The current state sets are intentionally included, for the
% use of reachable.

wave(Sos1, Machine, Sos2) :-
    setof1(S2,
           Symbol^S1^(hasSymbol(Machine, Symbol), 
                      member(S1, Sos1), 
                      targets(S1, Symbol, Machine, S2)),
           Sos3),
    union(Sos1, Sos3, Sos4),
    extensions(Sos4, Machine, Sos2).


% union(S, T, U) means that U is the union of sets S and T

union(S, T, U) :- setof1(Q, (member(Q, S);member(Q,T)), U).


% member(A, X) means that A is member of set X

member(A, [A | _]).
member(A, [_ | X]) :- member(A, X).


% test cases for conversion:

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

testCase(2, 
    machine([a],
            [[a, 0, b], [a, 0, c], [c, 1, e], [e, 0, b], [b, 0, c], [b, 1, d]],
            [d])).            


testCase(3,
    machine([q0],
            [[q0, a], [a, 0, b], [b, 1, b], [b, 0, c], 
             [q0, d], [d, 0, d], [d, 1, f], [f, 0, f]],
            [c, f])).            


% show a machine with a reasonably nice format

showMachine(Machine) :-
    hasStates(Machine, States),
    write('states = '), write(States), nl,

    hasStarting(Machine, Starting),
    write('starting = '), write(Starting), nl,

    hasAccepting(Machine, Accepting),
    write('accepting = '), write(Accepting), nl,

    hasTransitions(Machine, Transitions),
    listTransitions(Transitions).


% listTransitions shows a list of Transitions, one element per line

listTransitions([]).
listTransitions([A | X]) :-
  write('    '), write(A), nl,
  listTransitions(X).


% Test testCase I.

test(I) :- testCase(I, NondeterministicMachine),
           nl, write('Nondeterministic machine:'), nl,
           showMachine(NondeterministicMachine),
           reachable(NondeterministicMachine, Reachable),
           nl, write('Reachable = '), write(Reachable), nl,
           convert(NondeterministicMachine, DeterministicMachine),
           nl, write('Deterministic machine:'), nl,
           showMachine(DeterministicMachine).


% Test all test cases.

test :-
    test(_),
    fail.
test.


/* Examples

| ?- test.

Nondeterministic machine:
states = [a,b,c,d,e]
starting = [a]
accepting = [d]
    [a,0,b]
    [a,0,c]
    [b,1,d]
    [c,1,e]

Reachable = [[],[a],[b,c],[d,e]]

Deterministic machine:
states = [[],[a],[b,c],[d,e]]
starting = [[a]]
accepting = [[d,e]]
    [[],0,[]]
    [[],1,[]]
    [[a],0,[b,c]]
    [[a],1,[]]
    [[b,c],0,[]]
    [[b,c],1,[d,e]]
    [[d,e],0,[]]
    [[d,e],1,[]]

Nondeterministic machine:
states = [a,b,c,d,e]
starting = [a]
accepting = [d]
    [a,0,b]
    [a,0,c]
    [c,1,e]
    [e,0,b]
    [b,0,c]
    [b,1,d]

Reachable = [[],[a],[b],[b,c],[c],[d],[d,e],[e]]

Deterministic machine:
states = [[],[a],[b],[b,c],[c],[d],[d,e],[e]]
starting = [[a]]
accepting = [[d],[d,e]]
    [[],0,[]]
    [[],1,[]]
    [[a],0,[b,c]]
    [[a],1,[]]
    [[b],0,[c]]
    [[b],1,[d]]
    [[b,c],0,[c]]
    [[b,c],1,[d,e]]
    [[c],0,[]]
    [[c],1,[e]]
    [[d],0,[]]
    [[d],1,[]]
    [[d,e],0,[b]]
    [[d,e],1,[]]
    [[e],0,[b]]
    [[e],1,[]]

Nondeterministic machine:
states = [a,b,c,d,f,q0]
starting = [q0]
accepting = [c,f]
    [q0,a]
    [a,0,b]
    [b,1,b]
    [b,0,c]
    [q0,d]
    [d,0,d]
    [d,1,f]
    [f,0,f]

Reachable = [[],[a,d,q0],[b],[b,d],[b,f],[c],[c,d],[c,f],[d],[f]]

Deterministic machine:
states = [[],[a,d,q0],[b],[b,d],[b,f],[c],[c,d],[c,f],[d],[f]]
starting = [[a,d,q0]]
accepting = [[b,f],[c],[c,d],[c,f],[f]]
    [[],0,[]]
    [[],1,[]]
    [[a,d,q0],0,[b,d]]
    [[a,d,q0],1,[f]]
    [[b],0,[c]]
    [[b],1,[b]]
    [[b,d],0,[c,d]]
    [[b,d],1,[b,f]]
    [[b,f],0,[c,f]]
    [[b,f],1,[b]]
    [[c],0,[]]
    [[c],1,[]]
    [[c,d],0,[d]]
    [[c,d],1,[f]]
    [[c,f],0,[f]]
    [[c,f],1,[]]
    [[d],0,[d]]
    [[d],1,[f]]
    [[f],0,[f]]
    [[f],1,[]]

yes
*/