in model-checker .

fmod SEARCH is
pr META-LEVEL .
pr RANDOM .
including MODEL-CHECKER .


op _-_ : Nat Nat -> Nat .

op insertTerm : TermList Term -> TermList .

op lengthOfTrace : Trace -> Nat .

op getTrace : Trace -> TraceStep .

op getTraceTerm : TraceStep -> Term .

op getTraceType : TraceStep -> Type .

op trace2TermList : Qid Trace  -> TermList .

op getRule : Trace -> Rule .

op getRuleLabel : Rule -> Qid .

op getLabel : AttrSet -> Qid .

op getAllLabels : RuleSet -> QidList .

op getLabels : Module -> QidList .

op termApplyRule : Qid Term Qid -> Term .

op reverseTList : TermList -> TermList .

op termListLength : TermList -> Nat  .

op getTermList : TermList Nat -> TermList .

op getTermByIndex : TermList Nat -> Term .


op searchSequenceStates : Qid Term Term  Condition Qid Bound Nat -> TermList .






op getSolution : Trace Trace Qid Term Term  Condition Qid Bound Nat -> TermList .
op getTermFromTransList : TransitionList Nat -> Term .
op lengthTransList : TransitionList -> Nat .
op subShorter : Qid ModelCheckResult -> TermList .
op subloopSeqStates : Qid ModelCheckResult -> TermList .
op subDeadlockState : Qid ModelCheckResult -> Term .


op loopSeqStates : Qid State Formula -> TermList .
op shorter : Qid State Formula -> TermList .

op deadlockState : Qid State Formula -> Term .

vars transList transList1, transList2 : TransitionList .
var state : State .
var formula : Formula .
var trans : Transition .
var rlName : RuleName .


vars Mdl M C T L : Qid .
vars Mo Mod : Module .
vars I T1 T2 P TE TE1 TE2 : Term .
vars N N1 N2 Len Flag : Nat .
var B B2 : Bound .
vars TS TS2 : TraceStep .
var Trc preTrc : Trace .
vars TList TList1 TList2 TList3 TList12 TList21 : TermList .
var TY : Type .
vars RL R : Rule .
var Rls : RuleSet .
var Cond : Condition .
vars Attr AtS : AttrSet .

var R4Tup : Result4Tuple? .
var Lbls : QidList .




eq 0 - N = 0 .
eq s(N2) -  0 = s(N2) .
eq s(N2) - s(N) = N2 - N .


eq insertTerm(nil, TE) = (TE) .
eq insertTerm(empty, TE) = (TE) .
eq insertTerm((TE, TList), TE1) =  TE , insertTerm(TList, TE1) .


eq termListLength(empty) = 0 .
eq termListLength(nil) = 0 .
eq termListLength((TE, TList)) = 1 + termListLength(TList) .


eq getTermList(nil, N) = empty .
eq getTermList((TE, TList), 0) = empty .
eq getTermList((TE, TList), s(N)) = TE, getTermList(TList, N) .


eq getTermByIndex(empty, N) = nil .
eq getTermByIndex(nil, N) = nil .
eq getTermByIndex((TE, nil), 0) = TE .
eq getTermByIndex((TE, TList), 0) = TE .
eq getTermByIndex((TE, TList), N) = getTermByIndex(TList, N - 1) .

eq getTrace(TS Trc) = TS .
eq getTrace(TS) = TS .
eq getTrace(failure) = failure .
eq getTrace(nil) = nil .

eq getTraceTerm({TE,TY,RL}) = TE .
eq getTraceTerm(nil) = nil .
eq getTraceTerm({TE,TY,RL}) = TY .
eq getTraceTerm(nil) = nil .

eq getRule(nil) = none .
eq getRule({TE,TY,RL}) = RL .

eq getLabel(label(L) AtS) = L .
eq getLabel(AtS) = 'no-label [owise] .


eq getRuleLabel(none) = 'no-label  .
eq getRuleLabel(rl T1 => T2 [Attr]. ) = getLabel(Attr) .
eq getRuleLabel(crl(T1)=>(T2)if(Cond)[(Attr)].) = getLabel(Attr) .


eq termApplyRule(Mdl, nil, 'no-label) = nil .
eq termApplyRule(Mdl, TE, 'no-label) = nil .
eq termApplyRule(Mdl, nil, L ) = nil .
eq termApplyRule(Mdl, TE , L) = getTerm(metaXapply(upModule(Mdl, false), TE, L, none, 0, unbounded, 0)) .

eq trace2TermList(Mdl,nil) = empty .
eq trace2TermList(Mdl,failure) = empty .
eq trace2TermList(Mdl,TS) = getTraceTerm(TS) , termApplyRule(Mdl, getTraceTerm(TS), getRuleLabel(getRule(TS))) .
eq trace2TermList(Mdl,TS Trc) = getTraceTerm(TS), trace2TermList(Mdl,Trc) .


eq searchSequenceStates(M, I, P, Cond, T, B, N) = trace2TermList(M , metaSearchPath(upModule(M, false),I,P, Cond, T, B, N)) .


eq lengthTransList(nil) = 0 .
eq lengthTransList(trans transList) = 1 + lengthTransList(transList) .

eq getTermFromTransList(nil, N) = nil .
eq getTermFromTransList((({state, rlName}) transList), 0) = upTerm(state) .
eq getTermFromTransList((trans transList), N) = getTermFromTransList(transList, N - 1) .

eq subShorter(M, true) = nil .
eq subShorter(M, counterexample(transList1, transList2)) =

 searchSequenceStates(M, getTermFromTransList(transList1, 0) , getTermFromTransList(transList1,lengthTransList(transList1) - 1 ) , nil, '*, unbounded, 0) .


eq subloopSeqStates(M, true) = nil .
eq subloopSeqStates(M, counterexample(transList1, transList2)) =

searchSequenceStates(M, getTermFromTransList(transList2, 0) , getTermFromTransList(transList2,lengthTransList(transList2) - 1 ) , nil, '*, unbounded, 0) .


eq subDeadlockState(M, true) = nil .
eq subDeadlockState(M, counterexample(transList1, transList2)) = getTermFromTransList(transList2, 0) .




************ functions for generating counterexample ****

eq shorter(M, state, formula) = subShorter(M, modelCheck(state, formula)) .

eq loopSeqStates(M, state, formula) = subloopSeqStates(M, modelCheck(state, formula)) .

eq deadlockState(M, state, formula) = subDeadlockState(M, modelCheck(state, formula)) .
 ******************


op getAllSuccs :  Result4Tuple? Qid Term Qid Nat -> TermList  .
op findRuleSuccessors : Qid Term Qid   -> TermList .
op getAllSuccessors : Qid Term QidList -> TermList .

op tmpGenSeq : Qid Term Nat Bound QidList  TermList -> TermList .

op randNumber : Nat -> Nat .

eq randNumber(N) = random(N) .

op selNxt : TermList Nat -> Term .
op subGenSeq : Qid TermList Nat Bound QidList -> TermList .
op genSeq : Qid Term Nat Bound -> TermList .

eq getRule(nil) = none .
eq getRule({TE,TY,RL}) = RL .

eq getLabel(label(L) AtS) = L .
eq getLabel(AtS) = 'no-label [owise] .


eq getRuleLabel(none) = 'no-label  .
eq getRuleLabel(rl T1 => T2 [Attr]. ) = getLabel(Attr) .
eq getRuleLabel(crl(T1)=>(T2)if(Cond)[(Attr)].) = getLabel(Attr) .


eq getAllLabels(none) = nil .
eq getAllLabels(R Rls) = getRuleLabel(R) getAllLabels(Rls) .

eq getLabels(Mod) = getAllLabels(getRls(Mod)) .



eq getAllSuccs(failure , M, TE, L , N) = empty .
eq getAllSuccs(R4Tup , M, TE, L , N) = getTerm(R4Tup) , getAllSuccs(metaXapply(upModule(M, false), TE, L, none, 0, unbounded, N), M, TE, L, N + 1)  .



eq findRuleSuccessors(M, TE , L) =  getAllSuccs(metaXapply(upModule(M, false), TE, L, none, 0, unbounded, 0), M, TE, L, 1) .


eq getAllSuccessors(M, empty , Lbls) = empty .

eq getAllSuccessors(M, TE , nil) = empty .

eq getAllSuccessors(M, TE , (L Lbls)) = findRuleSuccessors(M, TE, L) , getAllSuccessors(M, TE , Lbls) .



eq selNxt(empty,N) = empty .
eq selNxt(TList,N) = getTermByIndex(TList,N rem termListLength(TList)) .

eq tmpGenSeq(M,I,N,0, Lbls, TList) = TList .
eq tmpGenSeq(M,empty,N,B, Lbls, TList) = TList .
eq tmpGenSeq(M,I,N,s(B), Lbls, TList)=   tmpGenSeq(M,selNxt(getAllSuccessors(M, I, Lbls),N),random(N quo 100000) ,B, Lbls, (TList, I)) .



eq genSeq(M,I,N,0) = empty .
eq genSeq(M,I,N,s(B))=  tmpGenSeq(M,selNxt(getAllSuccessors(M, I, getLabels(upModule(M, false))),N) ,N,B, getLabels(upModule(M, false)), I) .






endfm