% TESTED FEATURES: Horn Clauses, taken from PTD, defining and using reflexive and transitive relation
% EXPECTED OUTCOME: Safe
specification Horn_Refl_Trans_Unsafe
channel_model CCM

entity Environment
{
  types
    adt < message;

  symbols
    initial(adt): fact;
    final(adt): fact;
    lt (adt, adt): fact;

  clauses
    lt_refl: forall A. A->lt(A); %% OFMC does not terminate on this
    lt_trans(A,B,C):   A->lt(C) :- A->lt(B) & B->lt(C);

   symbols
     A0, A1, A2: adt;

   body {
     initial(A0); % with dummy start value
     if (A0->lt(?A1)) % A1 should be any value "weakly greater than" A0, e.g. A0 itself
     {
       if (A1->lt(?A2)) % A2 should be any value "weakly greater than" A1, e.g. A1 itself
         final(A2);
     }
   }

   goals
     negated_lt_okay: forall A0 A2.
        [](initial(A0) & final(A2) => !(A0->lt(A2)));

}