(define-theory diagrams (representation))
(in-theory 'diagrams)


(DEFINE-RELATION DIAGRAM-DIRECT-PREDECESSOR (?A ?B)
 "The fc component X has a direct predecessor Y.
Obviously it is not transitive."
 :IFF-DEF
 (AND (= (INVERSE DIAGRAM-DIRECT-SUCCESSOR)
         DIAGRAM-DIRECT-PREDECESSOR)
      (FLOW-CHART-COMPONENT ?A)
      (FLOW-CHART-COMPONENT ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE DIAGRAM-DIRECT-PREDECESSOR
       FLOW-CHART-COMPONENT)
      (DOMAIN DIAGRAM-DIRECT-PREDECESSOR
       FLOW-CHART-COMPONENT)))
(DEFINE-RELATION DIAGRAM-DIRECT-SUCCESSOR (?A ?B)
 "The fc component X has a direct successor Y.
Obviously it is not transitive."
 :DEF
 (AND (DIAGRAM-SUCCESSOR ?A ?B)
      (FLOW-CHART-COMPONENT ?A)
      (FLOW-CHART-COMPONENT ?B)))
(DEFINE-RELATION DIAGRAM-PREDECESSOR (?A ?B)
 "To be understood as 'diagram element x 
has predecessor y'. This is transitive."
 :IFF-DEF
 (AND (= (INVERSE DIAGRAM-SUCCESSOR) DIAGRAM-PREDECESSOR)
      (FLOW-CHART-COMPONENT ?A)
      (FLOW-CHART-COMPONENT ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE DIAGRAM-PREDECESSOR FLOW-CHART-COMPONENT)
      (DOMAIN DIAGRAM-PREDECESSOR FLOW-CHART-COMPONENT)))
(DEFINE-RELATION DIAGRAM-SUBDIVISION (?A ?B))
(DEFINE-RELATION DIAGRAM-SUBDIVISION-OF (?A ?B))
(DEFINE-RELATION DIAGRAM-SUCCESSOR (?A ?B)
 "To be understood as 'diagram element x 
has successor y'. This is transitive."
 :DEF
 (AND (REPRESENTATION-RELATION ?A ?B)
      (FLOW-CHART-COMPONENT ?A)
      (FLOW-CHART-COMPONENT ?B)))
(DEFINE-RELATION FIRST-NODE (?A ?B) :IFF-DEF
 (AND (= (INVERSE FIRST-NODE-OF) FIRST-NODE)
      (FLOW-CHART ?A)
      (FLOW-CHART-COMPONENT ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE FIRST-NODE FLOW-CHART-COMPONENT)
      (DOMAIN FIRST-NODE FLOW-CHART)))
(DEFINE-RELATION FIRST-NODE-OF (?A ?B) :IFF-DEF
 (AND (NOT (EXISTS ?W
            (AND (FLOW-CHART-COMPONENT ?W) (DIAGRAM-PREDECESSOR ?A ?W))))
      (REPRESENTATION-RELATION ?A ?B)
      (FLOW-CHART-COMPONENT ?A)
      (FLOW-CHART ?B)))
(DEFINE-RELATION LAST-NODE (?A ?B) :IFF-DEF
 (AND (= (INVERSE LAST-NODE-OF) LAST-NODE)
      (FLOW-CHART ?A)
      (FLOW-CHART-COMPONENT ?B))
 :AXIOM-CONSTRAINTS
 (AND (RANGE LAST-NODE FLOW-CHART-COMPONENT)
      (DOMAIN LAST-NODE FLOW-CHART)))
(DEFINE-RELATION LAST-NODE-OF (?A ?B) :DEF
 (AND (REPRESENTATION-RELATION ?A ?B)
      (FLOW-CHART-COMPONENT ?A)
      (FLOW-CHART ?B))
 :CONSTRAINTS
 (NOT (EXISTS ?W
       (AND (FLOW-CHART-COMPONENT ?W) (DIAGRAM-SUCCESSOR ?A ?W)))))
(DEFINE-CLASS CYCLE-NODE (?SELF)
:DEF (FC-NODE ?SELF) :CONSTRAINTS
 (DIAGRAM-SUCCESSOR ?SELF ?SELF))
(DEFINE-CLASS DIAGRAM (?SELF)
:DEF (VISUAL-DOCUMENT ?SELF)
 :CONSTRAINTS (VALUE-CARDINALITY ?SELF _STRUCTURED 1))
(DEFINE-CLASS DIAGRAM-OBJECT (?SELF)
:DEF
 (AND (VISUAL-DOCUMENT ?SELF)
      (EXISTS (?A) (AND (PART-OF ?SELF ?A) (DIAGRAM ?A))))
 :CONSTRAINTS (EXISTS (?B) (AND (REPRESENTED-BY ?SELF ?B) (ICON ?B))))
(DEFINE-CLASS FC-NODE (?SELF)
:DEF
 (AND (DIAGRAM-OBJECT ?SELF)
      (EXISTS (?A) (AND (PART-OF ?SELF ?A) (FLOW-CHART ?A))))
 :AXIOM-DEF
 (SUBCLASS-PARTITION FC-NODE
  (SETOF JOIN-NODE FORK-NODE SIMPLE-NODE CYCLE-NODE)))
(DEFINE-CLASS FLOW-CHART (?SELF)
:DEF
 (AND (DIAGRAM ?SELF)
      (EXISTS (?A) (AND (STRICTLY-DEPENDS-ON ?SELF ?A) (GRAPH-THEORY ?A))))
 :CONSTRAINTS
 (AND (VALUE-CARDINALITY ?SELF FIRST-NODE 1)
      (VALUE-CARDINALITY ?SELF LAST-NODE 1)
      (EXISTS (?B) (AND (PART ?SELF ?B) (FLOW-CHART-COMPONENT ?B)))))
(DEFINE-CLASS FLOW-CHART-COMPONENT (?SELF)
:IFF-DEF
 (AND (THING ?SELF) (OR (FLOW-CHART ?SELF) (FC-NODE ?SELF))) :AXIOM-DEF
 (THE-ARCHETYPE FLOW-CHART-COMPONENT REIFIED-PROPERTY))
(DEFINE-CLASS FORK-NODE (?SELF)
:IFF-DEF
 (AND (FC-NODE ?SELF)
      (MINIMUM-SLOT-CARDINALITY ?SELF DIAGRAM-DIRECT-SUCCESSOR 2)))
(DEFINE-CLASS GRAPH (?SELF)
:DEF
 (AND (DOCUMENT ?SELF)
      (EXISTS (?A) (AND (STRICTLY-DEPENDS-ON ?SELF ?A) (GRAPH-THEORY ?A))))
 :CONSTRAINTS (VALUE-CARDINALITY ?SELF _FORMAL 1) :AXIOM-DEF
 (THE-ARCHETYPE GRAPH REIFIED-PROPERTY))
(DEFINE-CLASS GRAPH-THEORY (?SELF)
:DEF (THEORY ?SELF))
(DEFINE-CLASS JOIN-NODE (?SELF) "This resynchronizes two or more
disjunct nodes."
 :IFF-DEF
 (AND (FC-NODE ?SELF)
      (MINIMUM-SLOT-CARDINALITY ?SELF DIAGRAM-DIRECT-PREDECESSOR 2)
      (EXISTS (?A) (AND (DIAGRAM-PREDECESSOR ?SELF ?A) (FORK-NODE ?A))))
 :AXIOM-DEF (THE-ARCHETYPE JOIN-NODE REIFIED-PROPERTY))
(DEFINE-CLASS LOOK-UP-TABLE (?SELF)
:DEF (TABLE ?SELF))
(DEFINE-CLASS PETRI-NET (?SELF)
 "Petri nets are an extension of state-transition 
diagrams, useful to represent parallel processes and scripts."
 :DEF
 (AND (DIAGRAM ?SELF)
      (EXISTS (?A) (AND (STRICTLY-DEPENDS-ON ?SELF ?A) (GRAPH-THEORY ?A)))))
(DEFINE-CLASS PN-ARROW (?SELF)
:DEF
 (AND (DIAGRAM-OBJECT ?SELF)
      (EXISTS (?A) (AND (PART-OF ?SELF ?A) (PETRI-NET ?A)))
      (EXISTS (?B)
              (AND (REPRESENTS ?SELF ?B)
                   (AND (TIME-SPAN ?B)
                        (EXISTS (?C) (AND (PRECEDES ?B ?C) (*PHASE ?C)))
                        (FORALL (?C ?D)
                         (=> (AND (PRECEDES ?B ?C) (PRECEDES ?B ?D))
                          (= ?C ?D))))))))
(DEFINE-CLASS PN-BAR (?SELF)
:DEF
 (AND (DIAGRAM-OBJECT ?SELF)
      (EXISTS (?A) (AND (PART-OF ?SELF ?A) (PETRI-NET ?A)))
      (EXISTS (?B) (AND (REPRESENTS ?SELF ?B) (*PHASE ?B)))))
(DEFINE-CLASS PN-CIRCLE (?SELF)
:DEF
 (AND (DIAGRAM-OBJECT ?SELF)
      (EXISTS (?A) (AND (PART-OF ?SELF ?A) (PETRI-NET ?A)))
      (EXISTS (?B) (AND (REPRESENTS ?SELF ?B) (*STATE ?B)))))
(DEFINE-CLASS SIMPLE-NODE (?SELF) "A node that is not a 'syntactic'
node, i.e. neither a branching, synchro, nor a cycle node."
 :DEF (FC-NODE ?SELF))
(DEFINE-CLASS STATE-TRANSITION-DIAGRAM (?SELF)
:DEF
 (AND (DIAGRAM ?SELF)
      (EXISTS (?A) (AND (STRICTLY-DEPENDS-ON ?SELF ?A) (GRAPH-THEORY ?A)))))
(DEFINE-CLASS STD-ARROW (?SELF)
:DEF
 (AND (DIAGRAM-OBJECT ?SELF)
      (EXISTS (?A) (AND (PART-OF ?SELF ?A) (STATE-TRANSITION-DIAGRAM ?A)))
      (EXISTS (?B) (AND (REPRESENTS ?SELF ?B) (*EVENT ?B)))))
(DEFINE-CLASS STD-CIRCLE (?SELF)
:DEF
 (AND (DIAGRAM-OBJECT ?SELF)
      (EXISTS (?A) (AND (PART-OF ?SELF ?A) (STATE-TRANSITION-DIAGRAM ?A)))
      (EXISTS (?B) (AND (REPRESENTS ?SELF ?B) (*STATE ?B)))))
(DEFINE-CLASS TABLE (?SELF)
:DEF (DIAGRAM ?SELF))
(DEFINE-CLASS THE-FIRST-NODE (?SELF)
:IFF-DEF
 (AND (FLOW-CHART-COMPONENT ?SELF)
      (VALUE-CARDINALITY ?SELF FIRST-NODE-OF 1)
      (VALUE-TYPE ?SELF FIRST-NODE-OF FLOW-CHART)))
(DEFINE-CLASS THE-LAST-NODE (?SELF)
:IFF-DEF
 (AND (FLOW-CHART-COMPONENT ?SELF)
      (VALUE-CARDINALITY ?SELF LAST-NODE-OF 1)
      (VALUE-TYPE ?SELF LAST-NODE-OF FLOW-CHART)))