#  *******    RULE 1   ********
#=======================================================
# the speed of the train while is away must be greater
# than 60 and less than 61
#=======================================================
speed1 = train1.speed;
forall it2_1: away1 {
       it2_1 always ((speed1 > 60) && (speed1 < 61))
};
 

#  *******    RULE 2  (DSL 5, T5)  ********
#=======================================================
# Train 1 and 2 can't cross at the same time
#=======================================================

cross2 = [train2.status == "crossing"];

forall c1 : [train1.status == "crossing"] {
       forall c2 : cross2 {
              !(c1 intersects c2)
      }
};

# OR

cross1 = [train1.status == "crossing"];

forall c1 : cross1 {
       forall c2 : cross2 {
              (end(c1) is_before [,] start(c2)) ||
              (end(c2) is_before [,] start(c1))
      }
};
#  *******    RULE 3   ********
#=======================================================
# After crossing, the train has to start reporting
#=======================================================

report1 = [train1.status == "reporting"];

forall c1 : cross1 {
       exists c2 : report1 {
              end(c1) == start(c2)
      }
};

#  *******    RULE 4  ********
#=======================================================
# After crossing, the train has to be reporting
#=======================================================
#JLF report1 is an interval
forall c1 : cross1 {
      c1 after report1
};
 

#  *******    RULE 5   ********
#=======================================================
# After waiting, the train has to be crossing
#=======================================================

wait1 = [train1.status == "waiting"];
wait2 = [train2.status == "waiting"];

forall c1 : wait1 {
      c1 after cross1
};

# In this case the result if false because of the last
# interval.

forall c2 : wait2 {
      c2 after cross2
};

#  *******    RULE 6   ********
#=======================================================
# Before reporting, the train was crossing
#=======================================================

forall c1 : report1 {
      c1 before cross1
};

#  *******    RULE 7   ********
#=======================================================
#  1 second after crossing, the report must be finished.
#=======================================================
 
forall c1 : cross1 {
       exists c2 : report1 {
           end(c1) -> end(c1)~> 1 include end(c2)
      }
};

#  *******    RULE 7   ********
#=======================================================
#  Within 4 and 6 miliseconds, the report must be finished.
#=======================================================
forall c1 : cross1 {
       exists c2 : report1 {
           end(c1)~> 0.004 -> end(c1)~> 0.006 include end(c2)
      }
};

# OR:

forall c1 : cross1 {
      exists c2 : report1 {
           (time(end(c1)) <= time(start(c2))) &&
           (time(end(c1)) <= time(start(c2)))
      }
};

# ----------------------------------------------
#
# Basic examples
#
# ----------------------------------------------

#  *******    RULE (DSL 8)   ********
#=======================================================
# always the speed have to be possitive.
#=======================================================

-> always (train1.speed >= 0);

# OR

speed1 = train1.speed;
-> always (speed1 >= 0);

# but sometimes is waiting so, this should be false.
-> always (speed1 > 0);

#  *******    RULE (DSL 14)   ********
#=======================================================
# Allways, the duration of crossing has to be greater than 2 msec.
# and less than 15 msec.
#=======================================================
forall a_1:cross1 {
    (duration(a_1) > 0.002) &&
    (duration(a_1) < 0.015)
};

#  *******    RULE (DSL 17, 20, 21, 22, 24 and 25)  ********
#=======================================================
# the status of the train is never unknown.
#=======================================================
unknown = [train1.status == "unknown"];
cardinal( unknown ) == 0;

#  *******    RULE (DSL 27, 28)   ********
#=======================================================
# if the train is not waiting, it has to be moving (speed >0).
#=======================================================
not_waiting1 = -> -- wait1;
moving = [train1.speed >0];
empty = not_waiting1 -- moving;
cardinal(empty) == 0;
empty = moving -- not_waiting1;
cardinal(empty) == 0;
 

# ----------------------------------------------
#
# Relations between actions
#
# ----------------------------------------------

#  *******    RULE (DSL 12)   ********
#=======================================================
# After the train is away, it has to be crossing or waiting
#=======================================================
after_away1 = wait1 union cross1;
forall a_1:away1 {
       exists a2_1:after_away1 {
              a_1 after a2_1
        }
};

# OR

forall a_1:away1 {
              a_1 after after_away1
};

#  *******    RULE T1, T4    ********
#=======================================================
#  between 4 and 6 miliseconds
#  after crossing, the report must be finished.
#=======================================================
forall c1 : cross1 {
       exists c2 : report1 {
           time(end(c1)) > (time(end(c2)) - 0.006) &&
           time(end(c1)) < (time(end(c2)) - 0.004)
      }
};

#  *******    RULE    ********
#=======================================================
# The train can't go from away to report without crossing
#=======================================================
away_report1 = end(away1) -> start(report1);

forall a2_1:away_report1 {
       exists a1_1:cross1 {
              a2_1 include a1_1
        }
};

# NOTE: An interval
# include the start event but not the end. That explains why
# the first print returns true and the second false.
a2_1 include start(a2_1);
a2_1 include end(a2_1);

#  *******    RULE (DSL 9)   ********
#=======================================================
# if train 1 is not waiting, then it has to be crossing, away
# or reporting.
#=======================================================
cross_away_rep1 = cross1 union away1 union report1;
not_wait1 = -> -- wait1;
cardinal(cross_away_rep1 -- not_wait1)== 0;

# OR BETTER

cross_away_rep1 = cross1 | away1 | report1;
not_wait1 = -> -- wait1;
cardinal(cross_away_rep1 -- not_wait1)== 0;

#  *******    RULE    ********
#=======================================================
# train 1 can be either waiting or in one of these states:
#  crossing, away or reporting.
#=======================================================
cross_away_rep1 = cross1 | away1 |  report1;
not_wait1 = -> -- wait1;
(cardinal(cross_away_rep1 -- not_wait1) == 0) &&
       (cardinal(not_wait1 -- cross_away_rep1) == 0);

# OR
#  PROBLEMS WITH THE NULL INTERVALS!!!

forall a_1:wait1 {
        forall a2_1:cross_away_rep1 {
               !(a2_1 intersects a_1)
        }
 };

#  *******    RULE 6   ********
#=======================================================
# 1 milisecond before start reporting, the semaphore must
# be in green
#=======================================================
one_msec_bef =  0.001 <~ start(report1);
trail_in_green = [train1.semaphore == "green"];
forall e1_1:one_msec_bef {
     exists a1_1:trail_in_green {
               (a1_1 include e1_1)
      }
 };
 
# OR

train1semaphore = train1.semaphore;
forall a1_1:report1 {
           0.001 <~ start(a1_1) -> start(a1_1) begin
               (train1semaphore == "green")
};
# printclock x;
#  *******    RULE 6   ********
#=======================================================
# 1 milisecond before start reporting, the semaphore must
# be in green and must keep in red at least until start
# reporting.
#=======================================================
one_msec_bef_int = 0.001 <~ start(report1) -> start(report1);
trail_in_green = [train1.semaphore == "green"];
forall a2_1:one_msec_bef_int {
     exists a1_1:trail_in_green {
               (a1_1 include a2_1)
     }
};
 
# OR
# A SOLUTION VERY TIME CONSUMING:
forall a1_1:report1 {
           0.001 <~ start(a1_1) -> start(a1_1) always
               (train1semaphore == "green")
};
 

#  *******    RULE 6   ********
#=======================================================
# only one train can be waiting on the first trail
# this is, between two crossing only one arrival is possible
#=======================================================
btw_cross1 = end(cross1) -> end(cross1);
forall a1_1:btw_cross1 {
       (cardinal(tmp:wait1 st start(tmp) inside a1_1) == 1)
};

#  *******    RULE 6 (GENERAL CASE)  ********
#=======================================================
# only N trains can be waiting on the first trail
# this is, between two crossing only one arrival is possible
#=======================================================
N = 10;
before_cross1 =  <- start(cross1);
forall a1_1:before_cross1 {
       (cardinal(tmp:wait1 st start(tmp) inside a1_1) <=
            (N + cardinal(tmp:cross1 st start(tmp) inside a1_1)))
};
 

#  *******    RULE   ********
#=======================================================
# in a interval of T msec the train 1 can't change the speed in
# more than max;
#=======================================================
T = 0.001;
max = 70;
speed1 = train1.speed;
# forall a1_1:train1. ->train1.~>T {
#       tmp = (speed1 - speed1[time(start(a1_1))]);
#        a1_1 always ((tmp < max) &&
#                    (tmp > (-max)))
# };
forall a1_1:train1. ->train1.~>T {
       a1_1 always (((speed1 - speed1[time(start(a1_1))]) < max) &&
                     ((speed1 - speed1[time(start(a1_1))]) > (0-max)))
};

#=======================================================
#
#               END OF FILE
#
#=======================================================