solver-database.maude

fmod TRANSITION-TERM is
    pr 2TUPLE{Term,Qid} * (
        op `(_`,_`) to <_`,_>,
        op p1_ to getState,
        op p2_ to getLabel,
        sort Tuple{Term,Qid} to TransitionTerm) .
endfm

view TransitionTerm from TRIV to TRANSITION-TERM is
    sort Elt to TransitionTerm .
endv

fmod TRANSITION-TERM-LIST is
    pr LIST{TransitionTerm} * (sort NeList{TransitionTerm} to NeTransitionTermList, sort List{TransitionTerm} to TransitionTermList) .
endfm

fmod TRACE is
    pr 2TUPLE{Term,Nat} * (
        op `(_`,_`) to <_:_>,
        op p1_ to getState,
        op p2_ to getDepth,
        sort Tuple{Term,Nat} to Log) .
endfm

view Log from TRIV to TRACE is
    sort Elt to Log .
endv

fmod TRACE-LIST is
    pr LIST{Log} * (sort NeList{Log} to NeLogList, sort List{Log} to LogList) .
endfm

fmod STATES-&-CXSTATES is
    pr 2TUPLE{TermSet,TermSet} * (
        op `(_`,_`) to <_:_>,
        op p1_ to states,
        op p2_ to cxStates,
        sort Tuple{TermSet,TermSet} to States&CxStates) .
endfm

view States&CxStates from TRIV to STATES-&-CXSTATES is
    sort Elt to States&CxStates .
endv

view LogList from TRIV to TRACE-LIST is
    sort Elt to LogList .
endv

fmod NODE is
    pr 2TUPLE{States&CxStates,LogList} * (
        op `(_`,_`) to <_:_>,
        op p1_ to states&CxStates,
        op p2_ to logList,
        sort Tuple{States&CxStates,LogList} to Node) .
endfm

view Node from TRIV to NODE is
    sort Elt to Node .
endv

fmod NODESET is
    pr SET{Node} * (sort NeSet{Node} to NeNodeSet, sort Set{Node} to NodeSet) .
endfm

view NodeSet from TRIV to NODESET is
    sort Elt to NodeSet .
endv

fmod DATABASE-EXT-DECL is
    pr NODESET .

    sorts ConfigExt OCompExt .
    --- Prepare the sort of the result that be retured by checking
    sorts Result4Checking Result4Checking? .
    subsort Result4Checking < Result4Checking? .

    --- Define structure of message error as well as success
    op nil : -> Result4Checking [ctor] .
    op success : -> Result4Checking [ctor] .
    op {formula:_, term:_, trace:_, cx:_} : Term Term LogList Term -> Result4Checking? [ctor] .
    op getFormula : Result4Checking? -> Term .
    op getTerm : Result4Checking? -> Term .
    op getLogList : Result4Checking? -> LogList .
    op getCx : Result4Checking? -> Term .
    eq getFormula({formula: F:Term, term: T:Term, trace: L:LogList, cx: Cx:Term}) = F:Term .
    eq getTerm({formula: F:Term, term: T:Term, trace: L:LogList, cx: Cx:Term}) = T:Term .
    eq getLogList({formula: F:Term, term: T:Term, trace: L:LogList, cx: Cx:Term}) = L:LogList .
    eq getCx({formula: F:Term, term: T:Term, trace: L:LogList, cx: Cx:Term}) = Cx:Term .

    op (originModule:_) : ModuleExpression -> ConfigExt .
    op (reviseModule:_) : ModuleExpression -> ConfigExt .
    op (initState:_) : Term -> ConfigExt .
    op (leadsToFormula:_) : Term -> ConfigExt .
    op (eventuallyFormula:_) : Term -> ConfigExt .
    op (eleSort:_) : Sort -> ConfigExt .
    op (soupSort:_) : Sort -> ConfigExt .
    op (eventuallyProp:_) : Term -> ConfigExt .

    op (depthList:_) : NatList -> OCompExt .
    op (currentDepth:_) : Nat -> OCompExt .
    op (nodeSet:_) : NodeSet -> OCompExt .
    op (result:_) : Result4Checking? -> OCompExt .
endfm

view ConfigExt from TRIV to DATABASE-EXT-DECL is
    sort Elt to ConfigExt .
endv

view OCompExt from TRIV to DATABASE-EXT-DECL is
    sort Elt to OCompExt .
endv

fmod CONFIG-EXT&STATE-EXT is
    pr SET{ConfigExt} * (sort NeSet{ConfigExt} to NeConfigExtSet, sort Set{ConfigExt} to ConfigExtSet, op empty : -> Set{ConfigExt} to emptyConfigExt) .
    pr SET{OCompExt} * (sort NeSet{OCompExt} to NeOCompExtSet, sort Set{OCompExt} to OCompExtSet, op empty : -> Set{OCompExt} to emptyOCompExt) .
endfm

view ConfigExtSet from TRIV to CONFIG-EXT&STATE-EXT is
    sort Elt to ConfigExtSet .
endv

view OCompExtSet from TRIV to CONFIG-EXT&STATE-EXT is
    sort Elt to OCompExtSet .
endv

fmod DATABASE-EXT is
    pr META-UTILS .
    pr 2TUPLE{ConfigExtSet,OCompExtSet} * (op `(_`,_`) to `{_;_`},
        op p1_ to getConfig,
        op p2_ to getState,
        sort Tuple{ConfigExtSet,OCompExtSet} to DatabaseExt) .

    vars C : ConfigExt .
    vars Cs : ConfigExtSet .
    var Oc : OCompExt .
    vars OCs OCs' : OCompExtSet .
    vars DB-EXT : DatabaseExt .
    vars ME : ModuleExpression .
    vars T : Term .
    vars S : Sort .
    vars NL NL' : NatList .
    vars N N' : Nat .
    vars NS NS' : NodeSet .
    vars ND : Node .
    vars R4C R4C' : Result4Checking? .
    vars B : Bool .

    op sum : NatList -> Nat .
    eq sum(N NL) = N + sum(NL) .
    eq sum(nil) = 0 .

    op emptyDatabaseExt : -> DatabaseExt [ctor] .
    op isEmptyDatabaseExt : DatabaseExt -> Bool .
    ceq isEmptyDatabaseExt(DB-EXT) = true if DB-EXT == emptyDatabaseExt .
    eq isEmptyDatabaseExt(DB-EXT) = false [owise] .

    op getConfigExtSet : DatabaseExt -> ConfigExtSet .
    eq getConfigExtSet({ Cs ; OCs }) = Cs .
    op getOCompExtSet : DatabaseExt -> OCompExtSet .
    eq getOCompExtSet({ Cs ; OCs }) = OCs .

    op originModule : ConfigExtSet -> ModuleExpression .
    op reviseModule : ConfigExtSet -> ModuleExpression .
    op initState : ConfigExtSet -> Term .
    op leadsToFormula : ConfigExtSet -> Term .
    op eventuallyFormula : ConfigExtSet -> Term .
    op eventuallyProp : ConfigExtSet -> Term .
    op eleSort : ConfigExtSet -> Sort .
    op soupSort : ConfigExtSet -> Sort .

    eq originModule(((originModule: ME), Cs)) = ME .
    eq reviseModule(((reviseModule: ME), Cs)) = ME .
    eq initState(((initState: T), Cs)) = T .
    eq leadsToFormula(((leadsToFormula: T) , Cs)) = T .
    eq eventuallyFormula(((eventuallyFormula: T) , Cs)) = T .
    eq eventuallyProp(((eventuallyProp: T) , Cs)) = T .
    eq eleSort(((eleSort: S) , Cs)) = S .
    eq soupSort(((soupSort: S) , Cs)) = S .

    op depthList : OCompExtSet -> NatList .
    op currentDepth : OCompExtSet -> Nat .
    op nodeSet : OCompExtSet -> NodeSet .
    op result : OCompExtSet -> Result4Checking? .

    eq depthList(((depthList: NL), OCs)) = NL .
    eq currentDepth(((currentDepth: N), OCs)) = N .
    eq nodeSet(((nodeSet: NS), OCs)) = NS .
    eq result(((result: R4C), OCs)) = R4C .

    op clearDatabase : DatabaseExt -> DatabaseExt .
    eq clearDatabase({ Cs ; OCs }) = { Cs ; buildInitialOCompExtSet(initState(Cs), isCheckingLeadsTo(Cs)) } .

    op evalOCompExtSet : DatabaseExt OCompExtSet -> DatabaseExt .

    eq evalOCompExtSet({ Cs ; OCs }, (Oc , OCs'))
    = evalOCompExtSet($evalOCompExtSet({ Cs ; OCs }, Oc), OCs') .
    eq evalOCompExtSet({ Cs ; OCs }, emptyOCompExt) = { Cs ; OCs } .

    op $evalOCompExtSet : DatabaseExt OCompExt -> DatabaseExt .
    eq $evalOCompExtSet({ Cs ; ((depthList: NL), OCs) }, (depthList: NL'))
    = { Cs ; (depthList: NL'), OCs } .
    eq $evalOCompExtSet({ Cs ; ((currentDepth: N), OCs) }, (currentDepth: N'))
    = { Cs ; (currentDepth: N'), OCs } .
    eq $evalOCompExtSet({ Cs ; ((nodeSet: NS), OCs) }, (nodeSet: NS'))
    = { Cs ; ((nodeSet: NS'), OCs) } .
    eq $evalOCompExtSet({ Cs ; ((result: R4C), OCs) }, (result: R4C'))
    = { Cs ; ((result: R4C'), OCs) } .

    op isCheckingLeadsTo : ConfigExt -> Bool .
    eq isCheckingLeadsTo(((leadsToFormula: T), Cs)) = true .
    eq isCheckingLeadsTo(Cs) = false [owise] .
    op isCheckingEventually : ConfigExt -> Bool .
    eq isCheckingEventually(Cs) = not isCheckingLeadsTo(Cs) .
    
    op buildInitialOCompExtSet : Term Bool -> OCompExtSet .
    ceq buildInitialOCompExtSet(T, B)
        = (depthList: nil), (currentDepth: 0),
        ( nodeSet: < < addDepthToTerm(T) : emptyTermSet > : nil > ), (result: nil) if B .
    
    eq buildInitialOCompExtSet(T, B)
        = (depthList: nil), (currentDepth: 0),
        ( nodeSet: < < emptyTermSet : addDepthToTerm(T) > : nil > ), (result: nil) [owise] .

    op getNumberOfStates : NodeSet -> Nat .
    op getNumberOfCxStates : NodeSet -> Nat .
    eq getNumberOfStates((ND , NS)) = | states(states&CxStates(ND)) | + getNumberOfStates(NS) .
    eq getNumberOfStates(empty) = 0 .
    eq getNumberOfCxStates((ND , NS)) = | cxStates(states&CxStates(ND)) | + getNumberOfCxStates(NS) .
    eq getNumberOfCxStates(empty) = 0 .
endfm

view DatabaseExt from TRIV to DATABASE-EXT is
    sort Elt to DatabaseExt .
endv

fmod CHECKER is
    pr DATABASE-EXT .
    pr TERMSET-EXT .
    pr 2TUPLE{NodeSet,States&CxStates} * (
        op `(_`,_`) to <_:_>,
        op p1_ to ns,
        op p2_ to cache,
        sort Tuple{NodeSet,States&CxStates} to NodeSet&Cache) .

    pr TRANSITION-TERM-LIST .

    vars M : Module .
    vars NS NS1 NS2 : NodeSet .
    vars ND : Node .
    vars N D : Nat .
    vars L : NatList .
    vars LL : LogList .
    vars NeLL : NeLogList .
    vars DB-EXT : DatabaseExt .
    vars Cs : ConfigExtSet .
    vars OCs : OCompExtSet .
    vars T T' T1 T2 F P Cx : Term .
    vars RT : ResultTriple .
    vars TS TS1 TS2 : TermSet .
    vars STATES CxSTATES : TermSet .
    vars R4C : Result4Checking? .
    vars CACHE : States&CxStates .
    vars NS&CACHE : NodeSet&Cache .
    vars Q : Qid .

    op collect : Module NodeSet NatList Nat ConfigExtSet -> NodeSet .
    eq collect(M, NS, L, D, Cs) = $collect(M, NS, L, D, Cs) .

    --- update depth in module by stack up depth at each layer before execution
    op $collect : Module NodeSet NatList Nat ConfigExtSet -> NodeSet .
    eq $collect(M, NS, N L, D, Cs) = $collect(M, layerCheck(changeDepth(M, D + N), NS, D + N, Cs), L, D + N, Cs) [print "Depth = " D ", N = " N] .
    eq $collect(M, NS, nil, D, Cs) = NS [print "Depth = " D ", N = nil"] .

    --- Node : < < ALLStates : ALLCxStates > : < Term : Depth > | nil > >
    --- ALLStates :: TermSet : T1 | T2 | emptyTermSet
    --- NodeSet : [Node]+ , empty .
    op layerCheck : Module NodeSet Nat ConfigExtSet  -> NodeSet .
    eq layerCheck(M, NS, N, Cs) = $layerCheck(M, NS, N, empty, < emptyTermSet : emptyTermSet >, Cs) .

    op $layerCheck : Module NodeSet Nat NodeSet States&CxStates ConfigExtSet -> NodeSet .
    eq $layerCheck(M, empty, N, NS, CACHE, Cs) = NS .
    ceq $layerCheck(M, (ND , NS1), N, NS2, CACHE, Cs) = $layerCheck(
                                                M,
                                                NS1,
                                                N,
                                                union(NS2, ns(NS&CACHE)),
                                                cache(NS&CACHE),
                                                Cs
                                            ) if NS&CACHE := $$layerCheck(M, ND, N, empty, CACHE, Cs) .

    op $$layerCheck : Module Node Nat NodeSet States&CxStates ConfigExtSet -> NodeSet&Cache .
    eq $$layerCheck(M, < < emptyTermSet : emptyTermSet > : LL >, N, NS, CACHE, Cs) = < NS : CACHE > .
    ceq $$layerCheck(M, < < T | TS1 : TS2 > : LL >, N, NS, CACHE, Cs) = $$layerCheck(
                                                                M,
                                                                < < TS1 : TS2 > : LL >,
                                                                N,
                                                                union(
                                                                    NS,
                                                                    filterValidNode(
                                                                        < < (STATES except states(CACHE)) : (CxSTATES except cxStates(CACHE)) > : (< T : N > LL) >
                                                                    )
                                                                ),
                                                                < (STATES | states(CACHE)) : (CxSTATES | cxStates(CACHE)) >,
                                                                Cs
                                                            ) if STATES := genTermSet(M, T, N, Cs)
                                                            /\ CxSTATES := allCounterExample(M, T, leadsToFormula(Cs), eventuallyProp(Cs)) [print "Never come here if you are checking for eventually property"] .

    ceq $$layerCheck(M, < < emptyTermSet : T | TS2 > : LL >, N, NS, CACHE, Cs) = $$layerCheck(
                                                                M,
                                                                < < emptyTermSet : TS2 > : LL >,
                                                                N,
                                                                union(NS,
                                                                    filterValidNode(
                                                                        < < emptyTermSet : (CxSTATES except cxStates(CACHE)) > : (< T : N > LL) >
                                                                    )
                                                                ),
                                                                < states(CACHE) : (CxSTATES | cxStates(CACHE)) >,
                                                                Cs
                                                            ) if CxSTATES := allCounterExample(M, T, eventuallyFormula(Cs), eventuallyProp(Cs)) .

    --- Accept only either ALLStates or ALLCxStates are not empty
    op filterValidNode : NodeSet -> NodeSet .
    eq filterValidNode(empty) = empty .
    eq filterValidNode((< < TS1 : TS2 > : LL > , NS)) = if (size(TS1) == 0 and size(TS2) == 0)
                                                    then
                                                        filterValidNode(NS)
                                                    else
                                                        (< < TS1 : TS2 > : LL > , filterValidNode(NS))
                                                    fi .


    ************ GET ALL STATES AT A DEPTH ************
    op genTermSet : Module Term Nat ConfigExtSet -> TermSet .
    eq genTermSet(M, empty, D, Cs) = emptyTermSet .
    eq genTermSet(M, T, 0, Cs) = emptyTermSet .
    eq genTermSet(M, T, D, Cs) = $genTermSet(
        metaSearch(M, T, '`{_`}['__[getVarTerm(soupSort(Cs)), 'depth:_[upTerm(D)]]], nil, '*, unbounded, 0),
        M,
        T,
        D,
        0,
        Cs
    ) .

    op $genTermSet : ResultTriple? Module Term Nat Nat ConfigExtSet -> TermSet .
    eq $genTermSet(failure, M, T, D, N, Cs) = emptyTermSet .
    eq $genTermSet(RT, M, T, D, N, Cs) = getTerm(RT) | $genTermSet(
        metaSearch(M, T, '`{_`}['__[getVarTerm(soupSort(Cs)), 'depth:_[upTerm(D)]]], nil, '*, unbounded, N + 1),
        M,
        T,
        D,
        N + 1,
        Cs
    ) .

    ************ GET ALL COUNTEREXAMPLE STATES AT A DEPTH ************
    --- Build Equations to add to Module to ignore in next finding counterexample
    op buildEqs : Term Term -> EquationSet .
    eq buildEqs(T, P) = (eq '_|=_[T, P] = 'true.Bool [none] .) .
    --- eq buildEqs(T, P) = (eq '_|=_[T, 'inCs1.Prop] = 'true.Bool [none] .) .


    op allCounterExample : Module Term Term Term -> TermSet .
    eq allCounterExample(M, T, F, P) = $allCounterExample(M, T, F, P) .
    op $allCounterExample : Module Term Term Term -> TermSet .
    ceq $allCounterExample(M, T, F, P) = if (Cx :: Constant)
                                    then emptyTermSet
                                    else
                                        getCounterExampleState(Cx) | $allCounterExample(addEqs(buildEqs(getCounterExampleState(Cx), P), M), T, F, P)
                                    fi
                                    if Cx := getCounterExample(M, 'modelCheck[T, F]) .
    eq $allCounterExample(M, T, F, P) = emptyTermSet [owise] .

    op getCounterExampleState : Term -> TermList .
    eq getCounterExampleState(T) = topTL(extractTL(lastTL(extractTL(T)))) .

    --- Logic checking at the last layer with unbounded
    op lastLayerCheck : Module NodeSet ConfigExtSet -> Result4Checking? .
    eq lastLayerCheck(M, empty, Cs) = success .
    ceq lastLayerCheck(M, (ND , NS), Cs) = if R4C :: Result4Checking
                                        then
                                            lastLayerCheck(M, NS, Cs)
                                        else
                                            R4C
                                        fi
                                        if R4C := checkNode(M, ND, Cs) .

    --- Check counterexample in ALLStates one by one
    op checkStates : Module TermSet LogList ConfigExtSet -> Result4Checking? .
    eq checkStates(M, emptyTermSet, LL, Cs) = success .
    ceq checkStates(M, T | TS, LL, Cs) = if (Cx :: Constant)
                                    then checkStates(M, TS, LL, Cs)
                                    else
                                        {formula: F, term: T', trace: (< T : 0 > LL), cx: Cx}
                                    fi
                                    if T' := removeDepthFromTerm(T)
                                    /\ F := leadsToFormula(Cs)
                                    /\ Cx := getCounterExample(M, 'modelCheck[T', F]) .

    --- Check counterexample in ALLCxStates one by one
    op checkCxStates : Module TermSet LogList ConfigExtSet -> Result4Checking? .
    eq checkCxStates(M, emptyTermSet, LL, Cs) = success .
    ceq checkCxStates(M, T | TS, LL, Cs) = if (Cx :: Constant)
                                        then checkCxStates(M, TS, LL, Cs)
                                        else {formula: F, term: T', trace: (< T : 0 > LL), cx: Cx}
                                        fi
                                        if T' := removeDepthFromTerm(T)
                                        /\ F := eventuallyFormula(Cs)
                                        /\ Cx := getCounterExample(M, 'modelCheck[T', F]) .

    --- Check counterexample in a Node one by one in order, including both ALLStates and ALLCxStates
    op checkNode : Module Node ConfigExtSet -> Result4Checking? .
    ceq checkNode(M, ND, Cs) = if (R4C :: Result4Checking)
                    then checkCxStates(M, cxStates(states&CxStates(ND)), logList(ND), Cs)
                    else R4C
                    fi
                    if R4C := checkStates(M, states(states&CxStates(ND)), logList(ND), Cs) .
    eq checkNode(M, ND, Cs) = success [owise] .

    --- Building counterexample
    vars TTL : TransitionTermList .
    vars TT : TransitionTerm .

    op traceStepTerm : TraceStep -> Term .
    op traceStepRule : TraceStep -> Rule .
    eq traceStepTerm({ T:Term, T:Type, R:Rule }) = T:Term .
    eq traceStepRule({ T:Term, T:Type, R:Rule }) = R:Rule .

    op ruleLabel : Rule -> Term .
    eq ruleLabel(rl T1:Term => T2:Term [ label(Q:Qid) ].) = Q:Qid .
    eq ruleLabel(crl T1:Term => T2:Term if C:Condition [ label(Q:Qid) ].) = Q:Qid .


    op getQidTerm : Qid -> Term .
    eq getQidTerm(Q) = getTerm(metaParse(upModule('QID, false), qid("'" + string(Q)), 'Qid)) .

    op getTransitionList : Trace -> TransitionTermList .
    eq getTransitionList(nil) = nil .
    eq getTransitionList(TS:TraceStep T:Trace) = < traceStepTerm(TS:TraceStep), getQidTerm(ruleLabel(traceStepRule(TS:TraceStep))) > getTransitionList(T:Trace) .

    op getTrace : Module Term Term Nat -> Trace .
    ceq getTrace(M, T1, T2, N) = if T:Trace? == failure
                            then nil
                            else T:Trace?
                            fi
                            if T:Trace? := metaSearchPath(M, T1, T2, nil, '*, unbounded, 0) [print "\n Trace " T:Trace? ] .

    op buildCounterExample : Module LogList -> TransitionTermList .
    eq buildCounterExample(M, nil) = nil .
    eq buildCounterExample(M, < T : N > LL) = $buildCounterExample(M, T, LL, nil, N) .

    op $buildCounterExample : Module Term LogList TransitionTermList Nat -> TransitionTermList .
    eq $buildCounterExample(M, T, nil, TTL, D) = TTL .
    eq $buildCounterExample(M, T1, < T2 : N > LL, TTL, D) = $buildCounterExample(
        M, T2, LL,
        reverse(getTransitionList(getTrace(changeDepth(M, D), T1, T2, D))) TTL,
        D + N
    ) [print "\n T1 = " T1 "\n T2" T2 "\n D " D].

    op transformTransitionTermList : TransitionTermList -> TermList .
    eq transformTransitionTermList(nil) = empty .
    eq transformTransitionTermList(TT TTL) = '`{_`,_`}[removeDepthFromTerm(getState(TT)), getLabel(TT)], transformTransitionTermList(TTL) [print "TT " TT] .

    op combineCounterExample : TransitionTermList Term -> Term .
    eq combineCounterExample(TTL, 'counterexample['__[TL1:TermList], TL2:TermList]) = 'counterexample['__[transformTransitionTermList(TTL), TL1:TermList], TL2:TermList] .
    eq combineCounterExample(TTL, 'counterexample[TL1:TermList, TL2:TermList]) = 'counterexample['__[transformTransitionTermList(TTL), TL1:TermList], TL2:TermList] [owise] .

endfm