main(N,ACTIONSOCC,STATES):-
       setof(F,fluent(F),Lf), setof(A,action(A),La),
       setof(F,initially(F),Init), setof(F,goal(F),Goal),
       make_states(N,Lf,STATES),
       make_action_occurrences(N,La,ACTIONSOCC),
       set_initial(Init,STATES),
       set_goal(Goal,STATES),
       set_transitions(ACTIONSOCC,STATES),
       set_executability(ACTIONSOCC,STATES),
       get_all_actions(ACTIONSOCC,AllActions),
       labeling([ff],AllActions).
make_states(0,_,[]):-!.
       make_states(N,List,[S|STATES]) :-
       N1 is N-1, make_states(N1,List,STATES),
       make_one_state(List,S).
make_one_state([],[]).
make_one_state([F|Fluents],[fluent(F,VarF)|VarFluents]) :-
       make_one_state(Fluents,VarFluents), VarF in 0..1.
make_action_occurrences(1,_,[]):-!.
make_action_occurrences(N,List,[Act|ActionsOcc]) :-
       N1 is N-1, make_action_occurrences(N1,List,ActionsOcc),
       make_one_action_occurrences(List,Act),
       get_action_list(Act,AList), sum(AList,#=,1).
make_one_action_occurrences([],[]).
make_one_action_occurrences([A|Actions],[action(A,OccA)|OccActs]) :-
       make_one_action_occurrences(Actions,OccActs), OccA in 0..1.
set_initial(List,[InitialState|_]) :-
       set_state(List,InitialState).
set_goal(List,States) :-
       last(States,FinalState),
       set_state(List,FinalState).
set_state([],_).
set_state([Fluent|Rest],State) :-
        (Fluent=mneg(F),!,member(fluent(F,0),State);
         member(fluent(Fluent,1),State)),
        set_state(Rest,State).
set_transitions(_Occurrences,[_States]) :- !.
set_transitions([O|Occurrences],[S1,S2|Rest]) :-
       set_transition(O,S1,S2,S1,S2),
       set_transitions(Occurrences,[S2|Rest]).
set_transition(_Occ,[],[],_,_).
set_transition(Occ,[fluent(F,IV)|R1],[fluent(F,EV)|R2],FromSt,ToSt):-
       set_one_fluent(F,IV,EV,Occ,FromSt,ToSt),
       set_transition(Occ,R1,R2,FromSt,ToSt).
set_one_fluent(Fl,IV,EV,Occurrence,FromSt,ToSt) :-
       findall([X,L],causes(X,Fl,L),Pos),findall([Y,M],causes(Y,mneg(Fl),M),Neg),
       build_sum_prod(Pos,nOccurrence,FromSt,PFormula,EV,p),
       build_sum_prod(Neg,Occurrence,FromSt,NFormula,EV,n),
       findall(P,caused(P,Fl),StatPos),findall(N,caused(N,mneg(Fl)),StatNeg),
       build_sum_stat(StatPos,ToSt,PStatPos,EV,p),
       build_sum_stat(StatNeg,ToSt,PStatNeg,EV,n),
       append(PFormula,PStatPos,Pos_Fl),
       append(NFormula,PStatNeg,Neg_Fl),
       sum(Pos_Fl,#=,Psum),
       sum(Neg_Fl,#=,Nsum),
       EV  #<=> ((Psum + IV - IV * Nsum) #> 0).
build_sum_prod([],_,_,[],_,_).
build_sum_prod([[Action,Prec]|Rest],Occurrence,State,[Flag|PF1],EV,Mode):-
       get_precondition_vars(Prec,State,ListPV),
       length(Prec,NPrec), sum(ListPV,#=,SumPrec),
       member(action(Action,VA),Occurrence),
       (VA #= 1 #/\ (SumPrec #= NPrec)) #<=> Flag,
       (Mode == p -> EV #>= Flag; Mode == n -> EV #=< 1-Flag),
       build_sum_prod(Rest,Occurrence,State,PF1,EV,Mode).
build_sum_stat([],_,[],_,_).
build_sum_stat([Cond|Others],State,[Flag|Fo],EV,Mode) :-
       get_precondition_vars(Cond,State,List),
       length(List,NL), sum(List,#=,Result),
       Flag #<=> (Result #= NL),
       (Mode == p -> EV #>= Flag; Mode == n -> EV #=< 1-Flag),
       build_sum_stat(Others,State,Fo,EV,Mode).
set_executability(ActionsOcc,States) :-
       setof([Act,C],executable(Act,C),Conds),
       set_executability1(ActionsOcc,States,Conds).
set_executability1([],[_],_).
set_executability1([AStep|ARest],[State|States],Conds) :-
       set_executability_sub(AStep,State,Conds),
       set_executability1(ARest,States,Conds).
set_executability_sub(_Step,_State,[]).
set_executability_sub(Step,State,[[Act,C]|CA]) :-
       member(action(Act,VA),Step),
       get_precondition_vars(C,State,Cs),
       length(Cs,NCs), sum(Cs,#=,Temporary),
       VA #=1 #=> Temporary #= NCs,
       set_executability_sub(Step,State,CA).
get_precondition_vars([],_,[]).
get_precondition_vars([P1|Rest],State,[F|LR]) :-
       get_precondition_vars(Rest,State,LR),
       (P1 = mneg(FN),!, member(fluent(FN,A),State), F #= 1-A;
        member(fluent(P1,F),State)).
get_all_actions([],[]).
get_all_actions([A|B],List) :-
       get_action_list(A,List1),get_all_actions(B,List2),
       append(List1,List2,List).
get_action_list([],[]).
get_action_list([action(_,V)|Rest],[V|MRest]) :-
       get_action_list(Rest,MRest).
