Model (
   Model_Name          => ejemplopaper.pte,
   System_Pip_Behaviour=> STRICT);

Processing_Resource (
   Type                   => Regular_Processor,
   Name                   => cpu,
   Max_Interrupt_Priority => 32767,
   Min_Interrupt_Priority => 1,
   Worst_ISR_Switch       => 0.00,
   Avg_ISR_Switch         => 0.00,
   Best_ISR_Switch        => 0.00,
   Speed_Factor           => 1.00);

Scheduler (
   Type            => Primary_Scheduler,
   Name            => cpu_scheduler,
   Host            => cpu,
   Policy          => 
      ( Type                 => Fixed_Priority,
        Worst_Context_Switch => 0.00,
        Avg_Context_Switch   => 0.00,
        Best_Context_Switch  => 0.00,
        Max_Priority         => 32767,
        Min_Priority         => 1));

Scheduling_Server (
   Type                       => Regular,
   Name                       => a,
   Server_Sched_Parameters    => 
      ( Type         => Non_Preemptible_FP_Policy,
        The_Priority => 4,
        Preassigned  => NO),
   Scheduler                  => cpu_scheduler);

Scheduling_Server (
   Type                       => Regular,
   Name                       => b,
   Server_Sched_Parameters    => 
      ( Type         => Non_Preemptible_FP_Policy,
        The_Priority => 3,
        Preassigned  => NO),
   Scheduler                  => cpu_scheduler);

Scheduling_Server (
   Type                       => Regular,
   Name                       => c,
   Server_Sched_Parameters    => 
      ( Type         => Non_Preemptible_FP_Policy,
        The_Priority => 2,
        Preassigned  => NO),
   Scheduler                  => cpu_scheduler);

Operation (
   Type                     => Enclosing,
   Name                     => a,
   Worst_Case_Execution_Time=> 3.00,
   Avg_Case_Execution_Time  => 3.000E+100,
   Best_Case_Execution_Time => 0.00);

Operation (
   Type                     => Enclosing,
   Name                     => b,
   Worst_Case_Execution_Time=> 1.00,
   Avg_Case_Execution_Time  => 1.000E+100,
   Best_Case_Execution_Time => 0.00);

Operation (
   Type                     => Enclosing,
   Name                     => c,
   Worst_Case_Execution_Time=> 3.50,
   Avg_Case_Execution_Time  => 3.500E+100,
   Best_Case_Execution_Time => 0.00);

Transaction (
   Type            => regular,
   Name            => a,
   External_Events => 
      ( ( Type       => Periodic,
          Name       => a.input,
          Period     => 12.000,
          Max_Jitter => 0.000,
          Phase      => 0.000)),
   Internal_Events => 
      ( ( Type => Regular,
          Name => a.output,
          Timing_Requirements => 
            ( Type             => Hard_Global_Deadline,
              Deadline         => 9.500,
              Referenced_Event => a.input))),
   Event_Handlers  => 
      ( (Type               => System_Timed_Activity,
         Input_Event        => a.input,
         Output_Event       => a.output,
         Activity_Operation => a,
         Activity_Server    => a)));

Transaction (
   Type            => regular,
   Name            => b,
   External_Events => 
      ( ( Type       => Periodic,
          Name       => b.input,
          Period     => 15.000,
          Max_Jitter => 0.000,
          Phase      => 0.000)),
   Internal_Events => 
      ( ( Type => Regular,
          Name => b.output,
          Timing_Requirements => 
            ( Type             => Hard_Global_Deadline,
              Deadline         => 8.000,
              Referenced_Event => b.input))),
   Event_Handlers  => 
      ( (Type               => System_Timed_Activity,
         Input_Event        => b.input,
         Output_Event       => b.output,
         Activity_Operation => b,
         Activity_Server    => b)));

Transaction (
   Type            => regular,
   Name            => c,
   External_Events => 
      ( ( Type       => Periodic,
          Name       => c.input,
          Period     => 17.500,
          Max_Jitter => 0.000,
          Phase      => 0.000)),
   Internal_Events => 
      ( ( Type => Regular,
          Name => c.output,
          Timing_Requirements => 
            ( Type             => Hard_Global_Deadline,
              Deadline         => 5.500,
              Referenced_Event => c.input))),
   Event_Handlers  => 
      ( (Type               => System_Timed_Activity,
         Input_Event        => c.input,
         Output_Event       => c.output,
         Activity_Operation => c,
         Activity_Server    => c)));

