Merge pull request #147 from HannaMk/master

adding some corrections + update SVL generation

src/backends/lnt/ocarina-backends-lnt-svl_generator.adb

@@ -66,6 +66,9 @@ package body Ocarina.Backends.LNT.Svl_Generator is
 
    procedure Make_Demo_Svl is
    begin
+      Write_Str ("% DEFAULT_MCL_LIBRARIES=");
+      Write_Quoted_Str ("standard.mcl");
+      Write_Line ("");
       --  LTS generation
       Write_Quoted_Str ("Main.bcg");
       Write_Str ("=  divbranching reduction of ");
@@ -83,28 +86,118 @@ package body Ocarina.Backends.LNT.Svl_Generator is
       Decrement_Indentation;
       Write_Indentation;
       Write_Line ("end property;");
-      --  adding deadlock property
-      Write_Line ("property Scheduling_Test (ID) is");
+
+      --  adding Scheduling_Test property
+      Write_Line ("property Scheduling_Test (ID)");
       Increment_Indentation;
       Write_Indentation;
-      Write_Quoted_Str ("Main_$ID.bcg");
-      Write_Str ("=");
+      Write_Quoted_Str ("Scheduling Test ");
+      Write_Line ("is");
       Write_Quoted_Str ("Main.bcg");
-      Write_Line ("|=");
+      Write_Line ("|= with evaluator3");
       Write_Indentation;
-      Write_Str ("[ true* . ");
+      Write_Str ("NEVER (");
       Write_Quoted_Str ("ACTIVATION_$ID !T_Error");
-      Write_Line (" ] false;");
+      Write_Line (");");
       Write_Indentation;
       Write_Line ("expected TRUE;");
       Decrement_Indentation;
       Write_Indentation;
       Write_Line ("end property;");
 
-      --  for I in 1 .. Thread_Number loop
-      --  Write_Line ("check Scheduling_Test (" & Integer'Image (I) & ");");
-      --  end loop;
+      for I in 1 .. Thread_Number loop
+         Write_Line ("check Scheduling_Test (" & Integer'Image (I) & ");");
+      end loop;
+
+      --  adding Connection property
+      Write_Line ("property Connection (ID)");
+      Increment_Indentation;
+      Write_Indentation;
+      Write_Quoted_Str ("Connection Test ");
+      Write_Line ("is");
+      Write_Quoted_Str ("Main.bcg");
+      Write_Line ("|= with evaluator3");
+      Write_Indentation;
+      Write_Str ("AFTER_1_INEVITABLE_2 ");
+      Write_Str ("('SEND_$ID !*' , 'RECEIVE_$ID !*')");
+      Write_Line (";");
+      Write_Indentation;
+      Write_Line ("expected TRUE;");
+      Decrement_Indentation;
+      Write_Indentation;
+      Write_Line ("end property;");
 
+      --  adding Is_Preempted property
+      Write_Line ("property Is_Preempted (ID)");
+      Increment_Indentation;
+      Write_Indentation;
+      Write_Quoted_Str ("Is_Preempted Test ");
+      Write_Line ("is");
+      Write_Quoted_Str ("Main.bcg");
+      Write_Line ("|= with evaluator3");
+      Write_Indentation;
+      Write_Str ("SOME (");
+      Write_Str ("true* .");
+      Write_Quoted_Str ("ACTIVATION_$ID !T_DISPATCH_PREEMPTION");
+      Write_Str (". true* . (");
+      Write_Quoted_Str ("ACTIVATION_$ID !T_PREEMPTION");
+      Write_Str (")* . true* . ");
+      Write_Quoted_Str ("ACTIVATION_$ID !T_PREEMPTION_COMPLETION");
+      Write_Line (");");
+      Write_Indentation;
+      Write_Line ("expected TRUE;");
+      Decrement_Indentation;
+      Write_Indentation;
+      Write_Line ("end property;");
+
+      for I in 1 .. Thread_Number loop
+         Write_Line ("check Is_Preempted (" & Integer'Image (I) & ");");
+      end loop;
+
+      --  adding Data_Loss property
+      Write_Line ("property Data_Loss (ID)");
+      Increment_Indentation;
+      Write_Indentation;
+      Write_Quoted_Str ("Between two consecutive SEND_$ID actions," &
+         " there is a RECEIVE_$ID");
+      Write_Line (" is");
+      Write_Quoted_Str ("Main.bcg");
+      Write_Line ("|= with evaluator3");
+      Write_Indentation;
+      Write_Str ("NEVER (");
+      Write_Str ("true* .");
+      Write_Quoted_Str ("SEND_$ID !AADLDATA");
+      Write_Str (". (not");
+      Write_Quoted_Str ("RECEIVE_$ID !AADLDATA");
+      Write_Str (")* .");
+      Write_Quoted_Str ("SEND_$ID !AADLDATA");
+      Write_Line (");");
+      Write_Indentation;
+      Write_Line ("expected TRUE;");
+      Decrement_Indentation;
+      Write_Indentation;
+      Write_Line ("end property;");
+
+      --  adding Transition property
+      Write_Line ("property Transition (TH_NAME, Si, Sj)");
+      Increment_Indentation;
+      Write_Indentation;
+      Write_Quoted_Str ("Thread $TH_NAME, being in state $Si," &
+         " the corresponding $Sj state is eventually reachable");
+      Write_Line (" is");
+      Write_Quoted_Str ("Main.bcg");
+      Write_Line ("|= with evaluator3");
+      Write_Indentation;
+      Write_Str ("AFTER_1_INEVITABLE_2 (");
+      Write_Quoted_Str ("DISPLAY_STATE !$TH_NAME !$Si");
+      Write_Str (",");
+      Write_Quoted_Str ("DISPLAY_STATE !$TH_NAME !$Sj");
+      Write_Line (");");
+      Write_Indentation;
+      Write_Line ("expected TRUE;");
+      Decrement_Indentation;
+      Write_Indentation;
+      Write_Line ("end property;");
    end Make_Demo_Svl;
 
 end Ocarina.Backends.LNT.Svl_Generator;

src/backends/lnt/ocarina-backends-lnt-tree_generator_processor.adb

@@ -288,7 +288,7 @@ package body Ocarina.Backends.LNT.Tree_Generator_Processor is
       Aux_Act_1 : Node_Id;
       Aux_Act_2 : Node_Id;
 
-      Is_Not_Periodic : Boolean := true;
+      Is_Not_Periodic : Boolean := false;
       Threads : Thread_Array := T;
       L_Processor_Gates   : List_Id;
       L_Thread_Activation : List_Id;
@@ -733,7 +733,6 @@ package body Ocarina.Backends.LNT.Tree_Generator_Processor is
                           (Make_Identifier ("+"),
                            Make_Identifier ("k"),
                            Make_Nat (1))))));
-
       if (Not_Periodic_Thread_Number > 0) then
          BLNu.Append_Node_To_List (Make_Assignment_Statement
                     (Make_Identifier ("Is_Activated"),
@@ -745,12 +744,7 @@ package body Ocarina.Backends.LNT.Tree_Generator_Processor is
                     (Make_Identifier ("k"),
                      Make_Nat (1))),
                      No_List,
-                     New_List (Make_Assignment_Statement
-                    (Make_Identifier ("k"),
-                      Make_Infix_Function_Call_Expression
-                          (Make_Identifier ("+"),
-                           Make_Identifier ("k"),
-                           Make_Nat (1))))), L_While);
+                     No_List), L_While);
 
       end if;
 

src/backends/lnt/ocarina-backends-lnt-tree_generator_thread.adb

@@ -226,6 +226,9 @@ package body Ocarina.Backends.LNT.Tree_Generator_Thread is
       Out_Loop : List_Id;
       In_Select : List_Id;
       Variable : Node_Id;
+      Ti : Node_Id;
+      Source_Transition_List : List_Id;
+      Destination_Transition : Node_Id;
 
       Thread_Identifier : constant Name_Id
         := AIN.Display_Name (AIN.Identifier (E));
@@ -306,6 +309,23 @@ package body Ocarina.Backends.LNT.Tree_Generator_Thread is
                      exit when No (Vi);
                   end loop;
                end if;
+               if not BANu.Is_Empty (BATN.Transitions (BA)) then
+                  Ti := BATN.First_Node (BATN.Transitions (BA));
+                  loop
+                     Ti := BATN.Transition (Ti);
+                     Source_Transition_List := BATN.Sources (Ti);
+                     Destination_Transition := BATN.Destination (Ti);
+                     --  if (STATE == S1) and (not (INPUT))
+                     --  then STATE := S1; ... end if;
+                     Put_Line (Image (BATN.Display_Name
+                     (Destination_Transition)));
+                     Put_Line (Image (BATN.Display_Name
+                     (BATN.First_Node (Source_Transition_List))));
+                     --  --- ----- --- --- ---
+                     Ti := BATN.Next_Node (Ti);
+                     exit when No (Ti);
+                  end loop;
+               end if;
             end if;
             S := AIN.Next_Node (S);
             exit when No (S);