// WARNING!
// does not compile using the current revision of the trunk of BIP2
// compatible only with the new syntax for time introduced in the real-time-branch
//
// model for periodic task with known execution times
// scheduling is based on rate monotonic policy (RM), i.e. a task T1 can preempt T2 if P1 < P2 (Pi is the period of Ti)

model preemptive

connector type Singleton(Port p)
  define [ p ]
end


connector type Pair(Port p, Port q)
  define [ p q ]
end

connector type Triple(Port p, Port q, Port r)
  define [ p q r ]
end


atomic type CPU
  export port Port get
  export port Port preempt
  export port Port release

  place IDLE, COMPUTE

  initial to IDLE

  on get     from IDLE    to COMPUTE
  on preempt from COMPUTE to COMPUTE
  on release from COMPUTE to IDLE
end


atomic type Task(int period, int exec_time)
  export port Port next
  export port Port complete
  export port Port get_cpu
  export port Port preempted
  clock x,y unit millisecond

  place WAIT_CPU, COMPUTE, WAIT_PERIOD

  initial to WAIT_CPU

  on get_cpu from WAIT_CPU to COMPUTE
    eager
    resume y

  on preempted from COMPUTE to WAIT_CPU
    freeze y

  on complete from COMPUTE to WAIT_PERIOD
    when y in [ exec_time, exec_time ]
    eager

  on next from WAIT_PERIOD to WAIT_CPU
    when x in [ period, period ]
    eager
    reset x,y
end


compound type System
  component CPU   cpu
  component Task  A(1000, 500)  // UA = 500 / 1000 = 0.5   U = UA + UB = 0.8 <= 0.82 (maximal bound for RM scheduling)
  component Task  B(10,   3)    // UB = 3 / 10     = 0.3
  
  connector Singleton nextA(A.next)
  connector Pair      getA(cpu.get,     A.get_cpu)
  connector Pair      completeA(cpu.release, A.complete)
  // RM policy: A connot preempt B => no connector Triple    preemptA(cpu.preempt, A.get_cpu, B.preempted)

  connector Singleton nextB(B.next)
  connector Pair      getB(cpu.get,     B.get_cpu)
  connector Pair      completeB(cpu.release, B.complete)
  connector Triple    preemptB(cpu.preempt, B.get_cpu, A.preempted)
end


component System system
  
end