package validation
public
  with Data_Model;
  with Deployment;

-----------------
-- Subprograms --
-----------------

subprogram spg_printer1
properties
  source_language => C;
  source_name     => "print_lot_of_stuff";
  source_text     => ("printer.c");
end spg_printer1;

subprogram spg_printer2
properties
  source_language => C;
  source_name     => "print_too_many_stuff";
  source_text     => ("printer.c");
end spg_printer2;

-------------
-- Threads --
-------------

thread thr_printer1
end thr_printer1;

thread implementation thr_printer1.i
calls
mycalls: {
  P_Spg : subprogram spg_printer1;
};
properties
  Dispatch_Protocol                  => Periodic;
  Period                             => 1000 Ms;
  Compute_Execution_time             => 0 ms .. 3 ms;
  Deadline                           => 1000 ms;
  Priority                           => 2;
  Source_Data_Size                   => 4 Bytes;
  Source_Code_Size                   => 2 Bytes;
  Source_Stack_Size                  => 2 Bytes;
end thr_printer1.i;

thread thr_printer2
end thr_printer2;

thread implementation thr_printer2.i
calls
mycalls: {
  Q_Spg : subprogram spg_printer2;
};
properties
  Dispatch_Protocol                  => Sporadic;
  Period                             => 10 Ms;
  deadline                           => 10 Ms;
  Compute_Execution_time             => 0 ms .. 3 ms;
  Priority                           => 1;
  Source_Data_Size                   => 4 Bytes;
  Source_Code_Size                   => 2 Bytes;
  Source_Stack_Size                  => 2 Bytes;
end thr_printer2.i;

processor native
properties
  Deployment::Execution_Platform => native;
end native;

processor implementation native.i
properties
   Scheduling_Protocol => (Posix_1003_Highest_Priority_First_Protocol);
   Priority_Range => 0 .. 255;
   Scheduler_Quantum => 0 Ms;
   Preemptive_Scheduler => true;
end native.i;

---------------
-- Processes --
---------------

process prs_printer
end prs_printer;

process implementation prs_printer.i
subcomponents
  p1        : thread validation::thr_printer1.i;
  p2        : thread validation::thr_printer2.i;
properties
   Source_Data_Size => 4 Bytes;
   Source_Code_Size => 2 Bytes;
end prs_printer.i;

memory ram
end ram;

memory implementation ram.i
properties
   Word_Size => 8 bits;
   Byte_Count => 1;
end ram.i;

------------
-- System --
------------

system mysystem
end mysystem;

system implementation mysystem.local
subcomponents
  Node   : process prs_printer.i;
  CPU    : processor native.i;
  RAM    : memory ram.i;
properties
  actual_processor_binding => (reference (CPU)) applies to Node;
  actual_memory_binding    => (reference (RAM)) applies to Node;
annex real_specification {**
   theorem Contains_Memories
      foreach s in system_set do
         mainmem        := {y in Memory_Set | is_subcomponent_of (y, s)};

         check ( (Cardinal (mainmem) > 0) and
                 (Property_Exists (mainmem, "Byte_Count"))
               );
   end Contains_Memories;
**};
annex real_specification {**
   theorem Check_Memory_And_Process_Mem
      foreach m in memory_set do
         prs            := {x in Process_Set | is_bound_to (m, x)};

         check ( ((Get_Property_Value (m, "Word_Size")) * (Get_Property_Value (m, "Byte_Count"))) >
                 ((sum(Get_Property_Value (prs, "Source_Data_Size")))+
                  (sum(Get_Property_Value (prs, "Source_Code_Size"))))
               );
   end Check_Memory_And_Process_Mem;
**};
annex real_specification {**
   theorem Check_Thread_And_Process_Mem
      foreach p in process_set do
         thrs           := {y in Thread_Set | is_subcomponent_of (y, p)};

         check ( (
                  (Sum (Get_Property_Value (thrs, "Source_Data_Size")))+
                  (Sum (Get_Property_Value (thrs, "Source_Code_Size")))+
                  (Sum (Get_Property_Value (thrs, "Source_Stack_Size")))
                 )
               <
                 ((Get_Property_Value (p, "Source_Data_Size"))+
                  (Get_Property_Value (p, "Source_Code_Size")))
               );
   end Check_Thread_And_Process_Mem;
**};
annex real_specification {**
   theorem Check_Processor_Compliance
      foreach p in processor_set do
         prs            := {x in Process_Set | is_bound_to (x, p)};
         thrs           := {y in Thread_Set  | is_subcomponent_of (y, prs)};

         check ( (Min(Get_Property_Value (thrs, "Priority")) > First (Get_Property_Value (p, "Priority_Range"))) and
                (Max (Get_Property_Value (thrs, "Priority")) < Last (Get_Property_Value (p, "Priority_Range"))));

   end Check_Processor_Compliance;
**};


end mysystem.local;

end validation;