% -*- mode: prolog -*-

%% Library of predicates for analyzing cpsa4dbprolog output

%% The cpsa4db and cpsa4dbprolog programs are used to analyze the
%% output of cpsa4.  They translate cpsa4 output into a Prolog database
%% that captures the essential features of the output in a form that
%% can be queried using all of the power and flexibility of Prolog.

%% cpsa4db assembles the skeletons in the output into a forest of
%% derivation trees.  cpsa4dbprolog then prints the forest in Prolog
%% syntax.  To be loadable by Prolog, the output must be sorted so
%% that clauses of one predicate are colocated.  The sorting program
%% provided in all dialects of Unix does the job.

%% The output should be used by SWI Prolog as strings must not be
%% atoms.  Load the file generated by cpsa4prolog using consult/1.
%% Next load your query.  This file contains useful predicates that
%% may help formulate your query.  The comments for each predicate are
%% intended help users understand the output format.

%% Copyright (c) 2024 The MITRE Corporation

%% This program is free software: you can redistribute it and/or
%% modify it under the terms of the BSD License as published by the
%% University of California.

%% PATHS

%% The predicate path(L, Ls) is true if Ls is a path through the
%% derivation tree that starts with label L and ends with the label of
%% a skeleton that is at the root of the tree that contains L.  The
%% path predicate uses the step/3 predicate to determine if a skeletion
%% was derived from another skeleton.

%% The step predicate defines a transition relation for individual
%% cpsa4 steps.  step(P, O, L) is true if a cpsa4 step that started at
%% the skeleton labeled P produced a skeleton labeled L using the
%% operation O.  Notice that the same skeleton can appear as the
%% result of a step starting at different skeletons.  This means the
%% path predicate can find more than one path to the root.

%% For the path predicate, the operation field information is not
%% used.

path(L, [L]) :-
    root(L).

path(L, [L|Ls]) :-
    step(P, _, L),
    path(P, Ls).

%% A derivation tree is really a directed acyclic graph.  If the links
%% used for seen children are removed, the derivation tree becomes a
%% true tree--every child has exactly one parent.  The child/2
%% predicate encodes that relation.  It is used to traverse the tree
%% without revisiting a skeleton twice.  One can use it to count the
%% number of skeletons in a tree, for example.  Here we use it to find
%% the terminal skeletons without deplicates.  A terminal node is one
%% that has no successors.

terminal(L) :-
    step(L, _, _), !,
    fail.
terminal(_).

acc(W, W).
acc(W, X) :-
    child(W, Y),
    acc(Y, X).

%% A query to find the terminal skeletons using these predicates follows.

%% ask(L) :-
%%    root(W), acc(W, L), terminal(L).

%% SKELETON ASSOCIATION LISTS

%% The body of a skeleton is available as an association list.  It can
%% be queried using has_key_val(L, K, V), where L is a skeleton label,
%% K is a key, and V is its value.

has_key_val(L, K, V) :-
    skel(L, A),
    assoc(A, K, V).

assoc([[K | V] | _], K, V).
assoc([_ | A], K, V) :-
    assoc(A, K, V).

%% A query to find the labels of skeletons that are not eventually
%% dead follows.

%% ask(L) :-
%%     root(W), acc(W, L), acc(L, X), terminal(X), \+has_key_val(X, dead, _).

%% ask_all(Ls) :-
%%     findall(L, ask(L), Ls).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Clauses for the Dynamic Logic Runtime
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

falsehood(_) :-
    false.

truth(_) :-
    true.

equal(_, A, A).

%%% Node TWA

ntwa(Ka, [Sa, I], O, Kb, [Sb, I]) :-
    stwa(Ka, Sa, O, Kb, Sb).

%%% Plus step -- one or more steps

step_plus(Ka, [O], Kb) :-
    step(Ka, O, Kb).
step_plus(Ka, [O|Os], Kb) :-
    step(Ka, O, Kc),
    step_plus(Kc, Os, Kb).

mtwa_plus(Ka, Ma, [O], Kb, Mb) :-
    mtwa(Ka, Ma, O, Kb, Mb).
mtwa_plus(Ka, Ma, [O|Os], Kb, Mb) :-
    mtwa(Ka, Ma, O, Kc, Mc),
    mtwa_plus(Kc, Mc, Os, Kb, Mb).

stwa_plus(Ka, Ma, [O], Kb, Mb) :-
    stwa(Ka, Ma, O, Kb, Mb).
stwa_plus(Ka, Ma, [O|Os], Kb, Mb) :-
    stwa(Ka, Ma, O, Kc, Mc),
    stwa_plus(Kc, Mc, Os, Kb, Mb).

ntwa_plus(Ka, Ma, [O], Kb, Mb) :-
    ntwa(Ka, Ma, O, Kb, Mb).
ntwa_plus(Ka, Ma, [O|Os], Kb, Mb) :-
    ntwa(Ka, Ma, O, Kc, Mc),
    ntwa_plus(Kc, Mc, Os, Kb, Mb).

%% Star step -- zero or more steps

step_star(K, [], K).
step_star(Ka, [O|Os], Kb) :-
    step(Ka, O, Kc),
    step_star(Kc, Os, Kb).

mtwa_star(K, M, [], K, M).
mtwa_star(Ka, Ma, [O|Os], Kb, Mb) :-
    mtwa(Ka, Ma, O, Kc, Mc),
    mtwa_star(Kc, Mc, Os, Kb, Mb).

stwa_star(K, M, [], K, M).
stwa_star(Ka, Ma, [O|Os], Kb, Mb) :-
    stwa(Ka, Ma, O, Kc, Mc),
    stwa_star(Kc, Mc, Os, Kb, Mb).

ntwa_star(K, M, [], K, M).
ntwa_star(Ka, Ma, [O|Os], Kb, Mb) :-
    ntwa(Ka, Ma, O, Kc, Mc),
    ntwa_star(Kc, Mc, Os, Kb, Mb).