;;; -*- Mode: LISP; Syntax: Common-lisp; -*-

;;;; Examples for Justification-based TMS
;; Last edited 1/29/93, by KDF

;;; Copyright (c) 1993, Kenneth D. Forbus, Northwestern University,
;;; and Johan de Kleer, the Xerox Corporation.
;;; All rights reserved.

;;; See the file legal.txt for a paragraph stating scope of permission
;;; and disclaimer of warranty.  The above copyright notice and that
;;; paragraph must be included in any separate copy of this file.

(in-package :cl-user)

(defun get-node (datum jtms)
  (dolist (node (jtms-nodes jtms))
    (if (equal datum (tms-node-datum node)) (return node))))

(defun get-justification (num jtms)
  (dolist (just (jtms-justs jtms))
    (if (= num (just-index just)) (return just))))

(proclaim '(special na nb nc nd ne nf ng contra *jtms*))

(defun ex1 ()
  (setq *jtms* (create-jtms "Simple Example" :debugging t)
	na (tms-create-node *jtms* 'a :assumptionp t)
	nb (tms-create-node *jtms* 'b :assumptionp t)
	nc (tms-create-node *jtms* 'c :assumptionp t)
	nd (tms-create-node *jtms* 'd :assumptionp t)
	ne (tms-create-node *jtms* 'e :assumptionp t)
	nf (tms-create-node *jtms* 'f :assumptionp t)
	ng (tms-create-node *jtms* 'g :assumptionp t))
  (justify-node 'j1 nf (list na nb))
  (justify-node 'j2 ne (list nb nc))
  (justify-node 'j3 ng (list na ne))
  (justify-node 'j4 ng (list nd ne))
  (enable-assumption na)
  (enable-assumption nb)
  (enable-assumption nc)
  (enable-assumption nd))

(defun ex2 () ;; uses Ex1 to test the contradiction stuff.
  (setq contra (tms-create-node *jtms* 'Loser :contradictoryp t))
  (justify-node 'j5 contra (list ne nf)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defvar assumption-a)
(defvar assumption-c)
(defvar assumption-e)
(defvar node-h)
(defvar node-g)
(defvar contradiction)


(defun ex3 ()
  (setq *jtms* (create-jtms "Multiple support example")
	assumption-a (tms-create-node *jtms* 'A :assumptionp t)
	assumption-c (tms-create-node *jtms* 'C :assumptionp t)
	assumption-e (tms-create-node *jtms* 'E :assumptionp t)
	node-h (tms-create-node *jtms* 'h))
  (enable-assumption assumption-a)
  (enable-assumption assumption-c)
  (enable-assumption assumption-e)
  (justify-node 'R1 node-h (list assumption-c assumption-e))
  (setq node-g (tms-create-node *jtms* 'g))
  (justify-node 'R2 node-g (list assumption-a assumption-c))
  (setq contradiction (tms-create-node *jtms*
				       'contradiction :contradictoryp t))
  (justify-node 'R3 contradiction (list node-g)))