;; This package of programs on LISP realizing constructs of 
;; set-theoretic declarative query language DELTA for complex 
;; nesting and cycling data 
;; (cf. also the WWW page on Bounded Set Theory accessible from  
;; http://www.botik.ru/~logic/) 
;; was written by Yury Serdyuk (Yury@serdyuk.botik.ru). 
;; (Sorry, all comments are only in Russian.)


;;   Подпрограмма MAKE-SE по графу graph и списку bsm_list
;;   пар бисимулирующих вершин, строит строго экстенсиональный
;;   граф se_graph, отмечая для вершины v в старом графе,
;;   ее новый (в общем случае) номер new_v в новом графе.
;;
(defun   MAKE-SE  ( graph bsm_list v  )
;;
 (PROG     (   curr_list   se_graph   ret_value  new_v )
;;
  (setq curr_list bsm_list )
  (setq se_graph  graph    )
  (setq new_v     v        )
;;
  loop
   ( if  (NULL curr_list)     (RETURN (list se_graph new_v )    )  ) 
;;
   (setq ret_value  (DEL_ONE_VRTX se_graph
                                  (first curr_list)
                                  (cdr curr_list  )
                                  new_v ) )
;;
   (setq se_graph   (first  ret_value) )
   (setq curr_list  (second ret_value) )
   (setq new_v      (third  ret_value) )
;;
   (GO loop)
 )
)
;;
;;   Подпрограмма DEL_ONE_VRTX по графу graph и паре pair = ( x y )
;;   его вершин,строит новый граф new_graph ,в котором
;;             a) исключена вершина y,  а
;;             б) началом ребер, выходивших из вершины y ,
;;                является вершина x .
;;   
;;   При этом 
;;             а) все вхождения y в список pairs_list заменяются на x ,
;;             б) для входной вершины v отмечается ее (возможно,новый)
;;                номер в графе new_graph.
;;
(defun DEL_ONE_VRTX ( graph  pair  pairs_list v  )
;;
  (PROG   ( x   y   new_v   new_graph   new_list )
;;
   (setq    x  (first  pair) )
   (setq    y  (second pair) )
;;
   (setq    new_graph  ( MODIFY_GRAPH graph x y      ) )
   (setq    new_list   ( MODIFY_PLIST x y pairs_list ) )
;;
   (if      (equal v y )  (setq new_v x     ) )
   (if      ( <    v y )  (setq new_v v     ) )
   (if      ( >    v y )  (setq new_v (1- v)) )
;;
   (RETURN  (list new_graph new_list new_v  ) )
  )
)
;;   Подпрограмма MODIFY_GRAPH исключает из графа graph вершину y,
;;   подставляя в качестве начала ребер, выходивших из этой вершины,
;;              бисимулярную ей вершину x.
;;                             
(defun MODIFY_GRAPH    ( graph   x   y )
 (PROG  ( new_k   desc_list   new_desc_list   new_desc  )
;;
;;   В новом графе вершин будет на 1 меньше, чем в старом
;;
  (setq new_k  (1-  (first graph))   )
;;  
;;   В цикле все описатели вершин старого графа ( за исключением
;;   описателя вершины y ) видоизменяются ( если это необходимо )
;;   и пересылаются в новый список описателей new_desc_list.
;;
  (setq desc_list     (second graph) )
  (setq new_desc_list NIL            )
;;
  loop
   (if   (NULL desc_list) (RETURN  (list  new_k  new_desc_list ))   )
;;
   (setq new_desc         (COMPUTE_NEW_DESC (first desc_list) x y ) )
;;
   (if   (NOT (NULL new_desc))  (setq   new_desc_list
                                        (cons new_desc   new_desc_list) ) )
   (setq desc_list  (cdr desc_list) )
   (GO loop)
 )
)
;;
;;   Подпрограмма COMPUTE_NEW_DESC по описанию desc вершины вида
;;                (  n  ( (a1 m1)   ...   (ar mr) ) )
;;   и паре вершин x и y, возвращает
;;         a) NIL   ,                          если n = y ,
;;         b) преобразованное описание вершины n , где , в частности ,
;;            mi заменяется на x, если mi = y, если n /= y.
;;
(defun COMPUTE_NEW_DESC   ( desc  x  y  )
 (PROG ( n  new_n  n_ch  m  new_m  pairs_list  new_pairs_list  atr )
;;
  (setq  n             (first desc) )
;;
  ( if   (equal n y )  (RETURN NIL) )
;;
  ( if   ( < n y)  ( setq new_n  n     ) )
  ( if   ( > n y)  ( setq new_n  (1- n)) )
;;
  (setq  n_ch  (second desc))
;;
  ( if   (ATOM n_ch)  (RETURN (list  new_n n_ch )) )
;;
  ( setq pairs_list     n_ch )
  ( setq new_pairs_list NIL  )
;;
;;   Обработка пар вида ( ai mi) из исходного описания desc
;;
  loop
;;
   ( if  (NULL pairs_list)      (RETURN (list new_n new_pairs_list)) )
;;
   (setq atr (first (first pairs_list)) )
   (setq m   (second(first pairs_list)) )
;;
   (if   (equal m y)  (setq new_m  x      ) )
   (if   ( >    m y)  (setq new_m  (1- m) ) )
   (if   ( <    m y)  (setq new_m  m      ) )
;;
   (setq new_pairs_list  (cons  (list atr new_m)   new_pairs_list ) )
   (setq pairs_list      (cdr   pairs_list )   )
   (GO loop)
 )
)
;;
;;   Подпрограмма MODIFY_PLIST для списка plist пар чисел вида
;;               (  ( n1 m1 )  ( n2 m2 )  ... ( nr mr )  )
;;   и чисел  x  и  y  :
;;    a) заменяет  ni(mi)   на x,          если  ni(mi) = y ,
;;    b) заменяет  ni(mi)   на ni-1(mi-1), если  ni(mi) > y ,
;;    c) оставляет ni(mi)   неизменным   , в противном случае.
;;
(defun MODIFY_PLIST  (  x   y   plist )
 (PROG ( curr_list   new_list   n   m   new_n   new_m )
;;
  (setq  curr_list  plist )
  (setq  new_list   NIL   )
;;
  loop
   (if   (NULL curr_list)   (RETURN new_list) )
;;
   (setq n  (first (first curr_list) ) )
   (setq m  (second(first curr_list) ) )
;;
   (COND (  (equal n y)  (setq new_n  x      ) )
         (  ( >    n y)  (setq new_n  (1-  n)) )  
         (  T            (setq new_n  n      ) )
   )
;;
   (COND (  (equal m y)  (setq new_m   x     ) )
         (  ( >    m y)  (setq new_m   (1- m)) )
         (  T            (setq new_m   m     ) )
   )
;;
   (setq new_list  (ADDIFNON (list new_n new_m) new_list)  )
   (setq curr_list (cdr curr_list)   )
   (GO   loop)
 )
)
;;****************************************************************
;;****************************************************************
;;****************************************************************
(defun BISIMULATION  ( graph n1 )
 (PROG  ( r0  r_curr  r-rest  r-new  )
;;
  (setq  r0     (COMPUTE_R0   n1   (-  (first graph) n1 )  ))
;;
  (setq  r_curr (COMPUTE_R1   graph  r0  )  )
;;
  (setq  r_rest (set-difference r0  r_curr ) )
;;
  loop
   (setq r_new  (COMPUTE_R_NEW graph r_rest r_curr ) )
   (if   (NULL r_new)   (RETURN  (set-difference r0 r_curr) ) )
;;
   (setq r_curr (union  r_curr r_new )        )
   (setq r_rest (set-difference r_rest r_new) ) 
   (GO loop)
 )
)
;;
;;
(defun COMPUTE_R0   ( n1 n2 )
;;
;;    n1 - количество вершин в g-graph'e
;;    n2 - количество вершин в h-graph'e
;;
;;    Подпрограмма COMPUTE_R0 вычисляет отношение
;;
;;      { (x y)  |  ( x@g_graph   & y@h_graph )  or
;;                  ( x,y@h_graph & Nx < Ny   )     }
;;
  (PROG   ( r0 count1 count2 )
;;
   (setq  count1   1   )
   (setq  count2   1   )
   (setq  r0       NIL )
;;
   loop1
    (if ( > count1 n1 )  (GO continue)  )
;;
    loop2
     (if ( > count2 n2 )  (PROG ()
                            (setq count2 1           )
                            (setq count1 (1+ count1) )
                            (GO   loop1              )
                           ) )
     (setq  r0     (cons (list count1 (+ n1 count2) )  r0)  )
     (setq  count2 (1+ count2) ) 
     (GO    loop2)
;;
   continue
;;
    (setq  count1  1 )
    (setq  count2  1 )
;;
    loop3
     (if ( > count1 n2 )   (RETURN r0 ) )
;;
     loop4
      (if ( > count2 n2)   (PROG  ()
                            (setq  count2  1           )
                            (setq  count1  (1+ count1) )
                            (GO    loop3)
                           ) )
      (if ( < count1 count2 ) (setq r0 (cons (list (+ n1 count1 )
                                                   (+ n1 count2 ) ) r0 ) ) )
      (setq count2  (1+ count2) )
      (GO   loop4)
 )
)
;;
;;   Подпрограмма COMPUTE_R1 строит начальное приближение r1 "небисимуляции"
;;                         на графе graph.
;;   В отношении r1 могут участвовать  только пары вершин из входного
;;                         отношения r0 .
;;
(defun COMPUTE_R1   ( graph  r0 )
 (PROG  ( r_curr   r1   x   y   x_ch   y_ch )
  (setq r_curr  r0  )
  (setq r1      NIL ) 
;;
  loop
   (if   (NULL r_curr)  (RETURN  r1)  )
;;
   (setq x  (first (first r_curr)) )
   (setq y  (second(first r_curr)) )
;;
   (setq x_ch (second (VERTEX_DESC graph  x )) )
   (setq y_ch (second (VERTEX_DESC graph  y )) )
;;
   (if ( or ( and (ATOM x_ch)
                  (ATOM y_ch)
                  (NOT  (equal x_ch y_ch))
            )
            ( and (ATOM x_ch       )
                  (NOT  (ATOM y_ch))
            )
            (and  (NOT  (ATOM x_ch))
                  (ATOM y_ch       )
            )
       )
       (setq r1 (cons (first r_curr) r1) )
   )
   (setq r_curr  ( cdr r_curr ) )
   (GO loop)
 )
)
;;
;;   Подпрограмма COMPUTE_R_NEW вычисляет очередное множество r_new
;;   "небисимулирующих" пар вершин на графе graph.
;;   Список r_rest     - исходное множество пар;
;;   список r_nonbisim - текущее множество "небисимулирующих" пар .
;;
(defun COMPUTE_R_NEW  ( graph   r_rest   r_nonbisim )
;;
 (PROG  ( r_curr  r_new  x  y )
;;
  (setq r_curr r_rest)
  (setq r_new  NIL   )
;;
  loop
   (if   (NULL r_curr)  (RETURN r_new) )
;;
   (setq x   (first (first r_curr)) )
   (setq y   (second(first r_curr)) )
;;
   (if   ( or ( NON_BISIM1 graph  x  y  r_nonbisim )
              ( NON_BISIM1 graph  y  x  r_nonbisim )
         )
         (setq r_new  (cons (first r_curr) r_new ) )
   )
   (setq r_curr (cdr r_curr) )
   (GO loop)
 )
)
;;
;;   Подпрограмма NON_BISIM1 вычисляет отрицание отношения одношаговой
;;   бисимуляции для вершин n  и  m  в графе graph на основе множества
;;   r_nonbisim "небисимулирующих" вершин
;; 
(defun  NON_BISIM1  ( graph  n  m  r_nonbisim )
;;
 (PROG  ( atr_a  atr_b  n_  m_  n_prdsrs  m_prdsrs  curr_prdsrs  )
;;
  (setq n_prdsrs  (second (VERTEX_DESC  graph  n ) )  )
  (setq m_prdsrs  (second (VERTEX_DESC  graph  m ) )  )
;;
  (  if (and (ATOM n_prdsrs)
             (ATOM m_prdsrs)
             (equal n_prdsrs m_prdsrs)) 
        (RETURN NIL) )
;;
  loop1
   ( if  (NULL n_prdsrs)    (RETURN  NIL)   )
;;
   (setq atr_a        (first  (first  n_prdsrs))  )
   (setq n_           (second (first  n_prdsrs))  )
   (setq curr_prdsrs  m_prdsrs                    )
;;
   loop2
;;
    ( if  (NULL curr_prdsrs)   (RETURN  T)  )
;;
    (setq atr_b  (first (first curr_prdsrs) ) )
    (setq m_     (second(first curr_prdsrs) ) )
;;
    ( if ( and ( equal atr_a  atr_b )
               (NOT (MY_MEMB  (list n_  m_ ) r_nonbisim ) )
               (NOT (MY_MEMB  (list m_  n_ ) r_nonbisim ) )
         )
         (PROG  ()  (setq n_prdsrs (cdr n_prdsrs) )
                    (GO loop1)
         )
    )
    (setq curr_prdsrs (cdr curr_prdsrs) )
    (GO   loop2)
 )
)
;;
;;   Подпрограмма ADD_HOR_GRAPH к исходному графу g_graph
;;   добавляет граф h_graph, который на входе программы задан в
;;   "горизонтальном" виде:
;;     ( ( atr1 (x1 cx1) (y1 cy1) )     ...    ( atrn (xn cxn) (yn cyn) ) ),
;;   где
;;       atri     - атрибут ребра xi --> yi ,
;;       cxi(cyi) - имя (идентификатор) вершины xi (yi), 
;;                  если она оказывается начальной  в достраиваемой
;;                  части графа .
;;
(defun  ADD_HOR_GRAPH  ( g_graph  h_graph )
;;
 (PROG  ( curr_n  h_matrix  corrspnd_list  curr_list  ret_value  )
;;
  (setq curr_n        (first g_graph) )
  (setq h_matrix      NIL             )
  (setq corrspnd_list NIL             )
  (setq curr_list     h_graph         )
;;
  loop
;;
  (if (NULL curr_list) (RETURN (list (list curr_n
                                           (append (second g_graph)
                                                   h_matrix)
                                     )
                                     corrspnd_list )) )
;;
  (setq ret_value (PUT_ONE_EDGE curr_n
                                h_matrix
                                corrspnd_list
                                (first curr_list) ) )
;;
  (setq curr_n        (first  ret_value) )
  (setq h_matrix      (second ret_value) )
  (setq corrspnd_list (third  ret_value) )
;;
  (setq curr_list     (cdr curr_list)    )
  (GO loop)
 )
)
;;
;;   Подпрограмма PUT_ONE_EDGE помещает ребро edge "горизонтального"
;;   графа,представленное в формате
;;                  (  atr   ( x  cx )   ( y cy )   )      ,
;;   в "вертикальный" граф , заданный списком h_matrix описаний своих
;;   вершин.
;;     При этом используется список соответствий corrspnd_list между
;;   номерами вершин в "горизонтальном" и "вертикальном" графах, и  
;;   общее текущее число curr_n вершин в строящемся новом графе.
;;
(defun  PUT_ONE_EDGE  ( curr_n  h_matrix  corrspnd_list  edge )
;;
 (PROG  ( x  y  number_x  number_y  x_desc  y_ch
          new_curr_n  curr_h_matrix  new_crspnd_list  component_y
          ret_value  )
;;
  (setq  x  ( first (second edge) ) )
  (setq  y  ( first (third  edge) ) )
;;
  (setq  new_curr_n      curr_n        )
  (setq  curr_h_matrix   h_matrix      )
  (setq  new_crspnd_list corrspnd_list )
;;
;;   Обработка вершины  y
;;
  (setq  number_y        (FIND_IN_CLIST corrspnd_list y ) )
;;
  (if (NOT (NULL number_y))
          (PROG ()
           (setq ret_value     (FIND-DELETE curr_h_matrix number_y ) )
           (setq component_y   (first ret_value)                     )
           (setq curr_h_matrix (second ret_value)                    ) 
          ))
;;
  (if (NULL number_y)
           (PROG ()
            (setq new_curr_n      (1+  new_curr_n) )
            (setq number_y        new_curr_n       )
            (setq new_crspnd_list (cons (list  y  number_y )
                                        new_crspnd_list )  )
            (setq component_y     (list  number_y
                                         (second (third edge)) ) )
           ))
;;
;;   Обработка вершины  x
;;
  (setq  number_x    (FIND_IN_CLIST new_crspnd_list  x  ) )
;;
  (if (NULL number_x)
           (PROG ()
            (setq new_curr_n      (1+ new_curr_n) )
            (setq number_x        new_curr_n      )
            (setq new_crspnd_list (cons (list  x  number_x )
                                        new_crspnd_list )  )
            (setq curr_h_matrix   (cons (list  number_x
                                               (second(second edge)) )
                                        curr_h_matrix ) )
           ))
;;
;;   Формирование нового описания для вершины  y
;;
  (setq  x_desc  (list   (first edge)  number_x ) )
  (setq  y_ch    (second component_y ) )
;;
  (COND  (  (ATOM y_ch)    (setq  component_y  (list  number_y
                                                      (list x_desc) ) ) )
         (  T              (setq  component_y  (list  number_y
                                                      (cons x_desc y_ch)) ))
  )
;;
;;   Добавление нового описания вершины  y  в строящийся граф
;;
  (setq  curr_h_matrix  ( cons component_y  curr_h_matrix ) )
;;
;;   Возврат измененных значений
;;
  ( RETURN   ( list  new_curr_n
                     curr_h_matrix
                     new_crspnd_list )  )
 )
)
;;
;;   Подпрограмма FIND_IN_CLIST в списке соответствий corrspnd_list вида
;;                (  ( n1  m1 )     ...   ( ns  ms )  )
;;   отыскивает  ni  равное  y .
;;   Если такое  ni  существует , то возвращается  mi ; в противном
;;   случае  - NIL .
;;
(defun FIND_IN_CLIST  ( corrspnd_list  y )
;;
 (PROG  ( curr_list   n  m )
;;
  (setq  curr_list  corrspnd_list )
;;
  loop
   ( if  (NULL curr_list)  (RETURN NIL)  )
;;
   (setq n  (first  (first curr_list))    )
   (setq m  (second (first curr_list))    )
;;
   ( if  (equal n y)  (RETURN m)      )
   (setq curr_list    (cdr curr_list) )
   (GO   loop)
 )
)
;;
;;   Подпрограмма FIND-DELETE в исходном списке in_list вида
;;    (   ( n1  ...  ) ( n2  ...  )  ...  ( nr   ... )  )  ,
;;   находит компоненту	, у которой ni = m , и возвращает спи-
;;   сок из найденной компоненты, и исходного списка, но уже
;;   без этой компоненты  .
;;
(defun FIND-DELETE   ( in_list  m )
 (PROG ( curr_list  result_list  component )
;;
  (setq curr_list   in_list )
  (setq result_list NIL     )
  (setq component   NIL     )
;;
  loop
   (if  (NULL curr_list) (RETURN  (list component result_list) ) )
;;
   (COND (  (equal m  (first(first curr_list)) )
                (setq component   (first curr_list) )  )
         (  T
                (setq result_list (cons (first curr_list) result_list)) )
   )
;;
   (setq curr_list (cdr curr_list) )
   (GO loop)
 )
)
;;
;;   Программа EXTRACT извлекает из графа g_graph "горизонтально"
;;   представленный в нем граф H , который задан в графе g_graph
;;   вершиной e .
;;   Формат возвращаемого списка result, представляющего граф H :
;;    ( (atr1 (x1 cx1) (y1 cy1))  ...  (atrn (xn cxn) (yn cyn)) ) ,
;;   где
;;      atri - атрибут ребра  xi --> yi ,
;;                 |~ имя (идентификатор) вершины cxi (cyi),    
;;      cxi(cyi) = |   eсли она является праэлементом в графе g_graph,
;;                 |_ NIL , в противном случае .
;;
(defun EXTRACT  ( g_graph  e )
;;
 (PROG ( pairs_list  result  attrib  pair  pair_x_y )
;;
  (setq  pairs_list  (ALL_PRS  g_graph  e ) )
  (setq  result      NIL                    )
;;
;;   Цикл перебора вершин , представляющих направленные ребра
;;                 "горизонтального" графа H
;;
  loop
   ( if ( NULL pairs_list )   (RETURN result)  )
;;
   (setq  attrib   (first (first pairs_list)  )  )
   (setq  pair     (second(first pairs_list)  )  )
   (setq  pair_x_y (EXTRACT_PAIR  g_graph pair)  )
;;
;;   Подпрограмма EXTRACT_PAIR возвращает ребро графа H
;;   в формате
;;             (  ( x cx )  ( y cy) )   ( см. выше ) .
;;
   (setq  result     (ADDIFNON (cons attrib pair_x_y ) result ) )
   (setq  pairs_list (cdr pairs_list) )
   (GO    loop)
 )
)
;;   
;;   Подпрограмма EXTRACT_PAIR в графе g_graph по вершине pair,
;;   представляющей упорядоченную пару <x,y>, извлекает номера
;;   вершин,обозначающих элементы x и y, и возвращает их в форма-
;;   те
;;          (  ( x cx )  ( y cy ) )  ,
;;   где
;;       cx,cy  - "характеристики" вершин x,y  ( см. комментарии
;;   к программе EXTRACT ).
;;
(defun EXTRACT_PAIR   ( g_graph  pair )
;;
 (PROG ( pred_list  x_y  x  y  cx  cy )
;;
  (setq  pred_list (ATR_CANCEL  (ALL_PRS g_graph pair) ) )
;;
;;   У вершины, представляющей упорядоченную пару , может существовать
;;   два или один непосредственный предок.
;;   Последний случай имеет место , когда упорядоченная пара имеет вид
;;   < x , x > , или, точнее, она представляется множеством
;;                        {  a:  { b: x } } .
;;
  ( if (equal (list-length pred_list)  1 )
              (setq x_y    (CASE_LENGTH_1  g_graph
                                           (first  pred_list) ) )   )
  ( if (equal (list-length pred_list)  2 )
              (setq x_y    (CASE_LENGTH_2  g_graph
                                           (first  pred_list)
                                           (second pred_list) ) )   )
;;
;;   Характеристика  cn  вершины  n  показывает , является ли вершина
;;   начальной или нет в графе g_graph .
;;
  (setq  x  (first  x_y)  )
  (setq  y  (second x_y)  )
;;
  (setq  cx (GET-CHARAC  g_graph  x ) )
  (setq  cy (GET-CHARAC  g_graph  y ) )
;;
  (RETURN   (list   (list  x  cx )   (list  y  cy )  )  )
 )
)
;;
(defun  CASE_LENGTH_1    ( g_graph  vertex )
;;
;;   Здесь вершина vertex обозначает множество  { a:x )
;;
 (PROG    ( x_vertex )
;;
  (setq   x_vertex   ( cadar (ALL_PRS  g_graph  vertex  )  )  )
  (RETURN (list  x_vertex  x_vertex ) )
 )
)
;;
(defun  CASE_LENGTH_2  ( g_graph  v1  v2 )
;;
;;   Здесь вершины v1 и v2 представляют множества
;;        { a:x }   и  { b:x, c:y }  ,
;;   причем заранее неизвестно, какая вершина какое из данных 
;;   множеств представляет .
;;
  (PROG  ( pred_v1  pred_v2  singleton_x  singleton_y )
;;
   (setq   pred_v1  (ATR_CANCEL   (ALL_PRS  g_graph  v1)) )
   (setq   pred_v2  (ATR_CANCEL   (ALL_PRS  g_graph  v2)) )
;
   (setq   singleton_x  (intersection pred_v1  pred_v2) )
   (setq   singleton_y  (union   (set-difference pred_v1 singleton_x)
                                 (set-difference pred_v2 singleton_x)
                        ) )
;;
   (if (NULL singleton_y)  (setq  singleton_y  singleton_x)) 
   (RETURN (cons (first singleton_x)  singleton_y ) )
 )
)
;;
;;   Подпрограмма GET-CHARAC для вершины v из графа graph выдает 
;;   ее "характеристику".
;;   Характеристика вершины - это :
;;       или  a) имя (идентификатор) праэлемента,
;;                   если вершина его обозначает;
;;       или  б) NIL  ,
;;                   если вершина обозначает пустое множество;
;;       или  в) список вершин, из которых идут дуги ( c cоответ-
;;               cтвующими атрибутами ) в данную вершину,
;;                   если вершина представляет некоторое множество.
;;
(defun GET-CHARAC   (  graph  v  )
;;
 (PROG ( result  matrix  number )
;;
  (setq  matrix  (second graph) )
;;
  loop
   (if (NULL matrix)   (RETURN NIL) )
;;
   (setq  number  (first  (first matrix)) )
   (setq  result  (second (first matrix)) )
;;
   (if    (equal v number)  (RETURN result) )
   (setq  matrix (cdr matrix) )
   (GO  loop)
 )
)
;;   Программа DECORATION по "горизонтальному" графу и выделенной
;;   в нем вершине, представленными , соответственно , вершинами
;;   e  и  v  в графе graph, вычисляет его "вертикальное" представ-
;;   ление , встраиваемое в исходный граф .
;;
(defun  DECORATION  (  graph  e  v  )
;;
 (PROG  ( g_graph  h_graph  ret_value  corrspnd_list
          new_v    bsm_rel  )
;;
  (setq h_graph       (EXTRACT       graph   e )  )
;;
  (setq ret_value     (ADD_HOR_GRAPH graph  h_graph ) )
;;
  (setq g_graph       (first  ret_value) )
  (setq corrspnd_list (second ret_value) )
;;
  (setq new_v         (FIND_IN_CLIST corrspnd_list v) )
;;
;;*********************************************************
  (print 'COMPUTE_BISIMULATION_BEGIN )
;;*********************************************************
  (setq bsm_rel       (BISIMULATION  g_graph (first graph) ) )
;;
;;******************************************************
  (print (list 'BISIMULATION_RELATION  bsm_rel) )
;;******************************************************
  (RETURN             (MAKE-SE       g_graph bsm_rel new_v ) )
;;
 )
)  
;;***************************************************************
;;***************************************************************
;;***************************************************************
(defun COMPUTE_FORMULA ( graph formula )
 (COND
  ( (ATOM  formula)             (list graph formula) )
  ( (equal (first  formula) '~) (NEGATION   graph (second formula) ) )   
  ( (equal (first  formula) 'A) (FORALL     graph (second formula)
                                                  (third  formula)
                                                  (fourth formula)
                                                  (fifth  formula) ) )
  ( (equal (first  formula) 'E) (EXIST      graph (second formula)
                                                  (third  formula)
                                                  (fourth formula)
                                                  (fifth  formula) ) )
  ( (equal (second formula) '@) (MEMBERSHIP graph (first  formula)
                                                  (third  formula) ) )
  ( (equal (second formula) '=) (EQUALITY   graph (first  formula)
                                                  (third  formula) ) ) 
  ( (equal (second formula) '&) (AND_FORM   graph (first  formula)
                                                  (third  formula) ) )
  ( T                           (OR_FORM    graph (first  formula)
                                                  (third  formula) ) )
 )
)
;;
;;
;;
(defun NEGATION ( graph formula )
 (PROG ( rv )
  (setq  rv (COMPUTE_FORMULA graph formula ) )
  (if (equal (second rv) T ) (RETURN (list (first rv) NIL) ) )
  (RETURN  (list (first rv) T) )
 )
)
;;
;;
;;
(defun FORALL ( graph atr_var var term formula )
 (PROG ( curr_graph rv prs_list result ground_form )

  (setq rv         (COMPUTE_TERM graph term) )
  (setq curr_graph (first rv) )
  (setq prs_list   (ALL_PRS curr_graph (second rv) ) )
  
  (setq result     T )

   loop
    (if   (equal result NIL) (RETURN (list curr_graph NIL ) ) )
    (if   (NULL  prs_list  ) (RETURN (list curr_graph T   ) ) )

    (setq ground_form (SUBSTITUTION formula var (cadar prs_list) ) )
    (setq ground_form (SUBSTITUTION ground_form atr_var (caar prs_list)))
  
    (setq rv          (COMPUTE_FORMULA curr_graph ground_form) )
    (setq curr_graph  (first  rv) )
    (setq result      (second rv) ) 
    (setq prs_list    (cdr prs_list) )
    (GO loop)
 )
)
;;
;;
(defun EXIST ( graph atr_var var term formula )
 (PROG ( curr_graph rv prs_list result ground_form )

  (setq rv         (COMPUTE_TERM graph term) )
  (setq curr_graph (first rv) )
  (setq prs_list   (ALL_PRS  curr_graph (second rv) ) )
  
  (setq result     NIL )
  
   loop
    (if   (equal result   T) (RETURN (list curr_graph T     ) ) )
    (if   (NULL  prs_list  ) (RETURN (list curr_graph NIL   ) ) )

    (setq ground_form (SUBSTITUTION formula var (cadar prs_list) ) )
    (setq ground_form (SUBSTITUTION ground_form atr_var (caar prs_list)))
  
    (setq rv          (COMPUTE_FORMULA curr_graph ground_form) )
    (setq curr_graph  (first  rv) )
    (setq result      (second rv) ) 
    (setq prs_list    (cdr prs_list) )
    (GO loop)
 )
)
;;
;;
;;
(defun MEMBERSHIP ( graph l term2 )
 (PROG ( curr_graph rv vertex vertex_list atr term1 )
  
  (setq atr        (first l)  )
  (setq term1      (second l) )
  
  (setq rv         (COMPUTE_TERM graph term1) )
  (setq curr_graph (first  rv) )
  (setq vertex     (second rv) )
  
  (setq rv          (COMPUTE_TERM curr_graph term2) )
  (setq curr_graph  (first  rv) ) 
  (setq vertex_list (ALL_PRS curr_graph (second rv) ) )

  (if (MY_MEMB  (list atr vertex) vertex_list)
      (RETURN     (list curr_graph T) )           )
  (RETURN (list curr_graph NIL) )
 )
)
;;
;;
;;
;;
(defun EQUALITY ( graph term1 term2 )
 (PROG ( curr_graph rv vertex1 vertex2 )
  
  (setq rv         (COMPUTE_TERM graph term1) )
  (setq curr_graph (first  rv) )
  (setq vertex1    (second rv) )
  
  (setq rv          (COMPUTE_TERM curr_graph term2) )
  (setq curr_graph  (first  rv) ) 
  (setq vertex2     (second rv) ) 

  (if (equal vertex1 vertex2) (RETURN (list curr_graph T) ) )
  (RETURN (list curr_graph NIL) )
 )
)
;;
;;
(defun AND_FORM ( graph form1 form2 )
 (PROG ( curr_graph rv value1 value2 )
  
  (setq rv         (COMPUTE_FORMULA graph form1) )
  (setq curr_graph (first  rv) )
  (setq value1    (second rv) )

      
  (setq rv          (COMPUTE_FORMULA curr_graph form2) )
  (setq curr_graph  (first  rv) ) 
  (setq value2      (second rv) )
 
    
  (RETURN (list curr_graph (AND value1 value2) ) )
 )
)
;;
;;
(defun OR_FORM ( graph form1 form2 )
 (PROG ( curr_graph rv value1 value2 )

  (setq rv         (COMPUTE_FORMULA graph form1) )
  (setq curr_graph (first  rv) )
  (setq value1    (second rv) )

  (setq rv          (COMPUTE_FORMULA curr_graph form2) )
  (setq curr_graph  (first  rv) ) 
  (setq value2      (second rv) )


  (RETURN (list curr_graph (OR value1 value2) ) )
 )
)
;;*************************************************************
;;*************************************************************
;;*************************************************************
(defun COMPUTE_TERM ( graph term )
;;
;;   Программа COMPUTE_TERM вычисляет терм term, не содержащий
;;   свободных переменных, на графе graph
;;
 (PROG    ( operation )
 
  ( if (ATOM term ) (RETURN (list graph term)) )
  (setq operation   (first term) )

  (if (equal operation 'ENUM )
                       (RETURN (COMP_ENM graph (cdr term))) )
  (if (equal operation 'U    )
                       (RETURN (COMP_UNS (COMPUTE_TERM graph
                                                       (second term)) )) )
  (if (equal operation 'TC   )
                       (RETURN (COMP_TC  (COMPUTE_TERM graph
                                                       (second term)) )) )
  (if (equal operation 'D    )
                       (RETURN (DECORATION graph (second term)
                                                 (third  term) )) ) 
  (if (equal operation 'FIX  )
                       (RETURN (FIXPOINT graph (second term)
                                               (third  term)
                                               (fourth term)
                                               (fifth  term)
                                               (sixth  term) ) ) )                     
  (RETURN    (S_IMAGE graph  (first  term)
                             (second term)
                             (third  term)
                             (fourth term)
                             (fifth  term) ) )
 )
)
;;
;;
;;
(defun COMP_ENM ( graph arg_list )
 (PROG ( result list1 curr_graph ret_value )
  
  (setq result     NIL      )
  (setq list1      arg_list )
  (setq curr_graph graph    )
  
  loop
   (if   (NULL list1)  (RETURN   (ENUM curr_graph result    ) ) )
   (setq ret_value     (COMPUTE_TERM curr_graph (cadar list1) ) )   
   (setq curr_graph    (first  ret_value) )
   (setq result        (ADDIFNON (list (caar list1)
                                       (second ret_value) )
                                 result ) )
   (setq list1         (cdr  list1 ) )
   (GO loop)
 )
)
;;
;;
(defun COMP_UNS ( arg )
  
  (UNIONSET (first  arg)
            (second arg) )
)
;;
;;
(defun COMP_TC ( arg )
  
  (TR_CLOS  (first  arg)
            (second arg) )
)  
;;
;;
(defun COMP_CLS ( graph term_e term_v )
 (PROG ( curr_graph rv e v )
        
  (setq curr_graph graph )
  (setq rv         (COMPUTE_TERM curr_graph term_e) )
  (setq curr_graph (first  rv) )
  (setq e          (second rv) )
  (setq rv         (COMPUTE_TERM curr_graph term_v) )
  (setq v          (second rv) )
  (RETURN          (COLLAPS (first rv) e v ) )
 )
)
;;************************************************************
;;************************************************************
;;************************************************************
;;************************************************************
(defun ENUM ( graph prs_list )


 (ADD_VRTX graph prs_list)
)
;;
;;
;;
;;
(defun ADD_VRTX ( graph prs_list )
;;
;;   Программа ADD_VRTX добавляет в граф graph вершину,
;;   непосредственными предками которой являются вершины из
;;   списка prs_list, если такой вершины в графе не было.
;;   В противном случае, возвращается старый граф и номер
;;   вершины в нем с указанными непосредственными предками.
;;
 (PROG  ( matrix answer lengthpl )

  (setq matrix   (second graph) )

  (setq lengthpl (list-length prs_list) )

   loop
    (if (NULL matrix) (RETURN (ADD1 (second graph)
                                    prs_list
                                    (1+ (first graph)) )
                      ) )
    (setq answer  (ADD2 (first matrix)
                        (cadar matrix) 
                        prs_list
                        lengthpl ) )
    (if (NOT (NULL answer)) (RETURN (list graph (car answer))) )
    (setq matrix (cdr matrix) )
    (GO loop)
 )  
)
;;
(defun ADD1 (matrix prs_list new_number)
;;
;;   Программа ADD1 возвращает:
;;     а) граф,составленный из вершин списка matrix и новой вершины
;;        new_number с непосредственными предками prs_list;
;;     б) номер новой вершины.
;;
 (list (list new_number
             (append matrix
                     (list (list new_number prs_list) ) )
       )
       new_number ) )
;;
(defun ADD2 ( vertex l_or_atom prs_list l2 )
;;
;;   Программа ADD2 проверяет имеет ли вершина vertex из графа
;;   в точности тех же непосредственных предков, которые перечислены
;;   в списке prs_list. Если "да" - возвращается номер этой вершины;
;;   если "нет" - возвращается NIL .
;;
 (PROG  ( l ) 
;;
  (if    (and (ATOM l_or_atom)
              (NOT  (NULL l_or_atom)))            (RETURN NIL) )  
  (if    (NOT (equal (list-length l_or_atom) l2) ) (RETURN NIL) )
;;  
  (setq  l    (second vertex) )

   loop
    (if   (NULL l)     (RETURN (list (car vertex))) ) 
    (if   (NOT (MY_MEMB  (car l) prs_list))  (RETURN NIL) )
    (setq l (cdr l) )
    (GO   loop)
 ) 
)
;;******************************************************************
;;******************************************************************
;;******************************************************************
;;******************************************************************
(defun UNIONSET (graph n)

 (ADD_VRTX graph (UN_SET1 graph (ALL_PRS graph n) ) )
)
;;
;;
(defun UN_SET1 (graph pred_list)
 (PROG ( result list1 )
   
   (setq result NIL )
   (setq list1  pred_list)
    loop
     (if (NULL list1) (RETURN result) )
     (setq result (MY_UNION result
                            (ALL_PRS graph (cadar list1) ) ) )

     (setq list1 (cdr list1) )
     (GO loop)
 ) )
;;****************************************************************
;;****************************************************************
;;****************************************************************
;;***   Функция TR_CLOS вычисляет транзитивное замыкание вершины n
;;***       в (возможно , нефундированном ) графе graph
;;***
(defun TR_CLOS (graph n)

  (ADD_VRTX  graph (TR_CLOS1 graph (ALL_PRS graph n) NIL ) )
           
)
;;
;;
(defun TR_CLOS1 (graph unchecked result )
;;
  (COND  ( (NULL unchecked) result )
         ( (MY_MEMB (first unchecked) result)
                    (TR_CLOS1 graph (cdr unchecked) result) )
         ( T        (TR_CLOS1 graph
                              (append (cdr unchecked) 
                                      (ALL_PRS graph (cadar unchecked)))
                              (cons   (first unchecked) result)  ) )
  ) 
)
;;*********************************************************************
;;*********************************************************************
;;*********************************************************************
;;*********************************************************************
(defun FIXPOINT ( graph q atr_var var term formula )
 (PROG ( rv curr_graph p work_formula curr_q new_q )

  (setq rv         (COMPUTE_TERM graph term) )
  (setq curr_graph (first  rv)               )
  (setq p          (second rv)               )

  (setq rv           (PRECOMP_FORM curr_graph formula) )
  (setq curr_graph   (first  rv)                       )
  (setq work_formula (second rv)                       )
;;
;;   "Добавление" немотонности
;;
;;  (setq work_formula (list (list (list atr_var var) '@ q) '! work_formula) )
;;
;;   Поиск вершины,обозначающей пустое множество
;;
  (setq rv           (ADD_VRTX curr_graph NIL ) )
;;
  (setq curr_graph   (first rv)                 )  
  (setq curr_q       (second rv)                )
 
 
   loop
 
    (setq rv (S_IMAGE curr_graph (list atr_var var) atr_var var p
                                               (SUBSTITUTION work_formula
                                                             q
                                                             curr_q   )) )
    (setq curr_graph (first rv ) )

    (setq new_q      (second rv) )

    (print (list 'OLD curr_q))
    (print (list 'NEW new_q))
    (print '****** )
    (if   (equal new_q curr_q) (RETURN (list curr_graph curr_q)) )
    (setq curr_q new_q)
    (GO loop)
 )
)
;;********************************************************************
;;********************************************************************
;;********************************************************************
(defun S_IMAGE ( graph image_term atr_var var set_term formula )
;;
;;   Программа S_IMAGE реализует конструкцию выделения и взятия образа
;;  { image_term(atr_var,var) | atr_var:var set_term & formula(atr_var,var)}
;;   на графе graph
 (PROG ( cur_graph prs_list ret_value result truth_value groud_form 
         work_formula )

  (setq ret_value (COMPUTE_TERM graph set_term) )
  (setq cur_graph (first ret_value) )
  (setq prs_list  (ALL_PRS  cur_graph (second ret_value) ) )

;;
;;   В списке prs_list хранятся значения, по которым пробегает
;;                 пара переменных (atr_var,var)
;;
  (setq result NIL)
;;
;;
;;   Предварительное вычисление формулы formula
;;
;;
  (setq ret_value    (PRECOMP_FORM cur_graph formula ) )
  (setq cur_graph    (first  ret_value) )
  (setq work_formula (second ret_value) )
;;
;;   Основной цикл
;; 
  loop
  
   (if   (NULL prs_list) (RETURN (ADD_VRTX cur_graph result) ) )
   
   (setq ground_form (SUBSTITUTION work_formula var     (cadar prs_list) ) )
   (setq ground_form (SUBSTITUTION ground_form  atr_var (caar  prs_list) ) )
      
   (setq ret_value   (COMPUTE_FORMULA  cur_graph ground_form ) )
                                            
   (setq cur_graph   (first  ret_value) )
   (setq truth_value (second ret_value) )

;;
;;   Значение truth_value есть вычисленное значение формулы formula
;;   на очередном элементе из списка prs_list на текущем графе cur_graph
;;
   (if   (NULL truth_value) (GO label1) )
;;
;;   Вычисление терма-образа
;;
   (COND ( (and (equal (list-length image_term) 2)
                (equal (first image_term) atr_var)
                (numberp (second image_term)     ) )
           (setq result (ADDIFNON (list (caar prs_list)
                                        (second image_term))
                                  result )) )
         ( (and (equal (list-length image_term) 2)
                (equal (first image_term) atr_var)
                (equal  (second image_term) var   ) )
           (setq result (ADDIFNON (first prs_list) result) ) )
         ( T
           (PROG ( w_image_term )
             (setq w_image_iterm  (SUBSTITUTION image_term
                                                var 
                                                (cadar prs_list) ) )
             (setq w_image_iterm  (SUBSTITUTION w_image_iterm
                                                atr_var
                                                (caar prs_list) ) )
             (setq ret_value   (COMPUTE_TERM cur_graph
                                             w_image_iterm) )
             (setq cur_graph     (first     ret_value) )
             (setq result        (ADDIFNON  (list (caar prs_list)
                                                  (second ret_value))
                                            result) )
           )
         )                         
    )
   label1

   (setq prs_list (cdr prs_list) )
   (GO loop)
 )
) 
;;
;;
;;
(defun PRECOMP_FORM ( graph formula )
 (PROG ( curr_form rv curr_graph )
  (setq curr_form  formula )
  (setq curr_graph graph   )
   loop
   
    (setq rv  (REDUCT_EXPR curr_graph curr_form ) )
   
    (if  (equal  curr_form (second rv) ) (RETURN (list curr_graph curr_form)))
    (setq curr_graph (first rv) )
    (setq curr_form  (second rv))
    (GO loop)
 )
)
;;
;;
(defun REDUCT_EXPR ( graph expr )
 (PROG ( curr_graph list1 result rv )

  (if (ATOM expr) (RETURN (list graph expr) ) )
  (if (and  (equal   (first expr) 'TC )
            (numberp (second expr)    ) )
                     (RETURN (TR_CLOS graph (second expr) ) ) )
  (if (and  (equal   (first expr) 'U  )
            (numberp (second expr)    ) )
                     (RETURN (UNIONSET graph (second expr) ) ) )
  (if (and  (equal    (first expr) 'ENUM)
            (ALL_NUMP (cdr expr)        ) )
                      (RETURN (COMP_ENM graph (cdr expr) ) ) )
  (if (and  (equal    (first  expr) 'D )
            (numberp  (second expr)   )
            (numberp  (third  expr)   ) )
                      (RETURN (DECORATION graph (second expr)
                                             (third  expr) ) ) )
  (setq curr_graph graph  )
  (setq list1      expr)
  (setq result     NIL    )
   loop
    (if   (NULL list1)    (RETURN (list curr_graph result)) )  
    (setq rv   (REDUCT_EXPR curr_graph (car list1) ) )
    (setq curr_graph (first rv) ) 
    (setq result (append result (cdr rv) ) )
    (setq list1  (cdr list1) )
    (GO loop)
 )
)
;;
;;
;;
(defun ALL_NUMP ( l )
 (cond  (  (NULL l)    T )
        (  T           (and (numberp  (cadar l))
                            (ALL_NUMP (cdr   l)) ) )
 )
)
;;********************************************************************
;;********************************************************************
;;********************************************************************
(defun SUBSTITUTION ( expr var value)
 (COND
  ( (AND  (ATOM expr)
          (equal expr var) )  value ) 
  ( (ATOM expr)               expr  )
  ( T                         (cons (SUBSTITUTION (car expr) var value)
                                    (SUBSTITUTION (cdr expr) var value) ) )
 )
)
;;   
;;
(defun FILTER_V  ( atr l )
;;
;;   Из списка l вида ( (a1 v1) (a2 v2) ... (ak vk) )
;;   функция FILTER_V выбирает элементы (aj vj), у которых
;;                       aj = atr   ,
;;   и возвращает список из выбранных таким образом элементов.
;;
 (PROG ( result list1 )
  
  (setq result NIL)
  (setq list1  l  )

   loop
    (if   (NULL list1)             (RETURN result) )
    (if   (equal (caar list1) atr) (setq result (cons (car list1) result)) )
    (setq list1  (cdr list1) )
    (GO   loop)
 )
)
;;
;;
(defun COMPUTE ( graph_file term_file )
 (setq graph_stream
       (open graph_file :direction :input ) )
 (setq term_stream
       (open term_file  :direction :input ) )

 (print (COMPUTE_TERM (read graph_stream)
                      (read term_stream ) ) )
 (close graph_stream)
 (close term_stream )
)
;;
(defun ADDIFNON (x l)
 (PROG ( l1 )
  (setq l1 l)
   loop
    (if   (NULL l1)           (RETURN (cons x l) ) )
    (if   (equal x (car l1) ) (RETURN l ) )
    (setq l1 (cdr l1) )  
    (GO loop)
 )
)
;;
;;
(defun MY_UNION ( list1 list2 )
 (PROG ( result curr_list )
  (setq result list1)
  (setq curr_list list2)

   loop
    (if (NULL curr_list) (RETURN result) )
    (setq result (ADDIFNON (car curr_list) result ) )
    (setq curr_list (cdr curr_list) )
    (GO loop)
 )
)
;;
(defun ATR_CANCEL ( l )
 (COND ( (NULL l)  NIL )
       ( T         (ADDIFNON (cadar l)
                             (ATR_CANCEL (cdr l) ) ) ) 
 )
) 
;;
(defun VERTEX_DESC ( graph n )
 (PROG  ( curr_gr )
   (setq curr_gr (second graph) )
 
    loop
     (if (equal (caar curr_gr) n )  (RETURN (car curr_gr) )  )
     (setq curr_gr (cdr curr_gr) )
     (GO loop )
 ) )
;;****************************************************************
;;****************************************************************
;;****************************************************************
(defun ALL_PRS (graph n)
;;   Вычисление всех непосредственных предшественников
;;         вершины n в графе graph
;;
  (PROG ( result )

   (setq result  (second (VERTEX_DESC  graph n )) )
   (if     (ATOM result)   (RETURN NIL) )
   (RETURN result)
  )
)
;;********************************************************************
;;********************************************************************
;;********************************************************************
(defun MY_MEMB ( element list )
 (COND ( (NULL list)                   NIL                           )
       ( (equal element (first list))  T                             )
       ( T                             (MY_MEMB element (cdr list) ) )
 )
)
;;*******************************************************************
;;*******************************************************************
;;*******************************************************************
(defun   QORD    (  n  )
 (PROG   ( graph  k  )
  (setq graph  (HORQOR  n )  )
;;
  (print graph)
;;
  (setq k      (first graph) )
  (print       (DECORATION graph  k  (1+ n) ) )
 )
)
;;*********************************************************
;;*********************************************************
;;*********************************************************
(defun   HORQOR  (  n  )
;;
 ( PROG ( k  matrix  pair  desc  count  i )
;;
  (setq   k  (+  (*  4  n)  2 ) )
  (setq   matrix NIL            )
;;
  (setq   desc   NIL )
;;
  (setq   count  0   )
;;
  loop1
   ( if  ( > count (1-  n))    (GO continue1) )
;;
   (setq desc  (cons  (list  'a (+ (- k n) count) )
                      desc ) )
   (setq count (1+    count) )
   (GO   loop1)
;;
 continue1
;;
   (setq  matrix ( cons  (list k desc)  matrix) )
;;
   (setq  count  0 )
   loop2
    (if  ( > count  (1- n) )   (GO  continue2)  )
;;
    (setq  pair  (list  (list  'a (+ n (* 2 count) 2) )
                        (list  'a (+ n (* 2 count) 3) )
                 ) )
    (setq  matrix (cons (list (+  (- k n) count )  pair )  
                        matrix ) )
    (setq  count  (1+  count ) )
    (GO    loop2)
;;
  continue2
;;
   (setq  i  1 )
   loop3
    (if   ( > i n )   (GO  continue3) )
;;
    (setq matrix  (cons  (list  (+ n (* 2 i))
                                (list (list 'a i))  )
                         matrix ) )
    (setq matrix  (cons  (list  (+ n (* 2 i) 1)
                                (list (list 'a i) (list 'a (1+ i)) ) )
                         matrix ) )
    (setq i  (1+ i) )
    (GO   loop3)
;;
   continue3
    (setq  i  1 )
    loop4
;;
     ( if ( > i (1+ n) )   (GO continue4)  )
;;
     (setq  matrix  (cons  (list  i  (1-  i) )  matrix  ) )
     (setq  i       (1+  i) )
     (GO  loop4)
;;
   continue4
     (RETURN  (list  k matrix) )
  )
)