ada/OpenUxAS
0
0
Fork 0
mirror of https://github.com/AdaCore/OpenUxAS.git synced 2026-02-12 13:07:16 -08:00
Code Issues Packages Projects Releases Wiki Activity

Complete silver-level proof of main functionality of Assignment Tree Branch Bound

Browse Source
This commit is contained in:
Joffrey Huguet
2021-03-31 11:27:48 +02:00
parent 5f28a40c35
commit a04e130b3b
4 changed files with 1397 additions and 337 deletions
Download Patch File Download Diff File Expand all files Collapse all files

26
src/ada/src/services/atbb/algebra.adb
View File

@@ -17,6 +17,31 @@ package body Algebra with SPARK_Mode is
Result : out Int64_Seq;
Encounter_Executed_Out : out Boolean);
---------------
-- Free_Tree --
---------------
procedure Free_Tree (X : in out Algebra_Tree)
is
procedure Internal_Free is new Ada.Unchecked_Deallocation
(Algebra_Tree_Cell, Algebra_Tree);
begin
if X /= null then
if X.all.Node_Kind = Operator then
declare
Children : Algebra_Tree_Array := Algebra_Tree_Array (X.all.Collection.Children);
begin
for J in Children'Range loop
Free_Tree (Children (J));
pragma Loop_Invariant (for all K in Children'First .. J => Children (K) = null);
end loop;
end;
end if;
Internal_Free (X);
end if;
end Free_Tree;
-----------------------------
-- Get_Next_Objectives_Ids --
-----------------------------
@@ -174,6 +199,7 @@ package body Algebra with SPARK_Mode is
(Formula : Unbounded_String;
Algebra : out not null Algebra_Tree)
is
pragma SPARK_Mode (Off);
Kind : Node_Kind_Type := Undefined;
Operator_Kind : Operator_Kind_Type := Undefined;
form : Unbounded_String := Formula;

30
src/ada/src/services/atbb/algebra.ads
View File

@@ -1,5 +1,6 @@
with Ada.Strings.Unbounded; use Ada.Strings.Unbounded;
with Common; use Common;
with Ada.Unchecked_Deallocation;
package Algebra with SPARK_Mode is
@@ -48,7 +49,13 @@ package Algebra with SPARK_Mode is
function Is_Present
(Algebra : access constant Algebra_Tree_Cell;
TaskOptionId : Int64)
return Boolean;
return Boolean
is
(case Algebra.Node_Kind is
when Action => TaskOptionId = Algebra.TaskOptionId,
when Operator => (for some J in 1 .. Algebra.Collection.Num_Children => Is_Present (Algebra.Collection.Children (J), TaskOptionId)),
when Undefined => False);
pragma Annotate (GNATprove, Terminating, Is_Present);
function Get_Next_Objectives_Ids
(Assignment : Int64_Seq;
@@ -56,21 +63,16 @@ package Algebra with SPARK_Mode is
return Int64_Seq
with
Post =>
(for all TaskOptionId of Get_Next_Objectives_Ids'Result =>
Is_Present (Algebra, TaskOptionId));
(for all ObjectiveId of Get_Next_Objectives_Ids'Result =>
(Is_Present (Algebra, ObjectiveId)
and then
not Contains (Assignment, Int64_Sequences.First, Last (Assignment), ObjectiveId)));
pragma Annotate (GNATprove, Terminating, Get_Next_Objectives_Ids);
-- Returns a sequence of TaskOptionIds corresponding to the next possible
-- actions considering Assignment.
private
function Is_Present
(Algebra : access constant Algebra_Tree_Cell;
TaskOptionId : Int64)
return Boolean
is
(case Algebra.Node_Kind is
when Action => TaskOptionId = Algebra.TaskOptionId,
when Operator => (for some J in 1 .. Algebra.Collection.Num_Children => Is_Present (Algebra.Collection.Children (J), TaskOptionId)),
when Undefined => False);
procedure Free_Tree (X : in out Algebra_Tree) with
Depends => (X => X),
Post => X = null;
end Algebra;

1525
src/ada/src/services/atbb/assignment_tree_branch_bound.adb
View File

File diff suppressed because it is too large Load Diff

153
src/ada/src/services/atbb/assignment_tree_branch_bound.ads
View File

@@ -3,7 +3,7 @@ with Ada.Containers.Functional_Maps;
with Assignment_Tree_Branch_Bound_Communication; use Assignment_Tree_Branch_Bound_Communication;
with Common; use Common;
with LMCP_Messages; use LMCP_Messages;
with Ada.Containers; use Ada.Containers;
package Assignment_Tree_Branch_Bound with SPARK_Mode is
type Cost_Function_Kind is (Minmax, Cumulative);
@@ -28,6 +28,9 @@ package Assignment_Tree_Branch_Bound with SPARK_Mode is
subtype Int64_TaskPlanOptions_Map_Map is
Int64_TPO_Map_Maps.Map (10, Int64_TPO_Map_Maps.Default_Modulus (10));
use Int64_TPO_Map_Maps;
use Int64_TPO_Map_Maps.Formal_Model;
package Int64_TaskPlanOptions_Map_Maps_P renames Int64_TPO_Map_Maps.Formal_Model.P;
package Int64_TaskPlanOptions_Map_Maps_K renames Int64_TPO_Map_Maps.Formal_Model.K;
package Int64_ACM_Maps is new Ada.Containers.Formal_Hashed_Maps
(Key_Type => Int64,
@@ -36,6 +39,9 @@ package Assignment_Tree_Branch_Bound with SPARK_Mode is
subtype Int64_AssignmentCostMatrix_Map is
Int64_ACM_Maps.Map (10, Int64_ACM_Maps.Default_Modulus (10));
use Int64_ACM_Maps;
use Int64_ACM_Maps.Formal_Model;
package Int64_AssignmentCostMatrix_Maps_P renames Int64_ACM_Maps.Formal_Model.P;
package Int64_AssignmentCostMatrix_Maps_K renames Int64_ACM_Maps.Formal_Model.K;
----------------------------
-- Annotation subprograms --
@@ -49,6 +55,29 @@ package Assignment_Tree_Branch_Bound with SPARK_Mode is
(Assignment_Cost_Matrix : AssignmentCostMatrix)
return Boolean;
function Travel_In_CostMatrix
(VehicleId : Int64;
DestOption : TaskOption;
Assignment_Cost_Matrix : AssignmentCostMatrix)
return Boolean;
function Travel_In_CostMatrix
(VehicleId : Int64;
InitOption, DestOption : TaskOption;
Assignment_Cost_Matrix : AssignmentCostMatrix)
return Boolean;
function All_Travels_In_CostMatrix
(Request : UniqueAutomationRequest;
TaskPlanOptions_Map : Int64_TPO_Map;
Matrix : AssignmentCostMatrix)
return Boolean;
function All_EligibleEntities_In_EntityList
(Request : UniqueAutomationRequest;
TaskPlanOptions_Map : Int64_TPO_Map)
return Boolean;
----------------------------------------
-- Assignment Tree Branch Bound types --
----------------------------------------
@@ -56,7 +85,8 @@ package Assignment_Tree_Branch_Bound with SPARK_Mode is
type Assignment_Tree_Branch_Bound_Configuration_Data is record
Cost_Function : Cost_Function_Kind := Minmax;
Number_Nodes_Maximum : Int64 := 0;
end record;
end record
with Predicate => Number_Nodes_Maximum >= 0;
type Assignment_Tree_Branch_Bound_State is record
m_uniqueAutomationRequests : Int64_UniqueAutomationRequest_Map;
@@ -65,10 +95,25 @@ package Assignment_Tree_Branch_Bound with SPARK_Mode is
end record with
Predicate =>
(for all ReqId of m_taskPlanOptions =>
Valid_TaskPlanOptions (Element (m_taskPlanOptions, ReqId)))
(Valid_TaskPlanOptions (Element (m_taskPlanOptions, ReqId))
and then
Contains (m_uniqueAutomationRequests, ReqId)
and then
All_EligibleEntities_In_EntityList
(Element (m_uniqueAutomationRequests, ReqId),
Element (m_taskPlanOptions, ReqId))))
and then
(for all ReqId of m_assignmentCostMatrixes =>
Valid_AssignmentCostMatrix (Element (m_assignmentCostMatrixes, ReqId)));
Valid_AssignmentCostMatrix (Element (m_assignmentCostMatrixes, ReqId))
and then
Contains (m_uniqueAutomationRequests, ReqId)
and then
Contains (m_taskPlanOptions, ReqId)
and then
All_Travels_In_CostMatrix
(Element (m_uniqueAutomationRequests, ReqId),
Element (m_taskPlanOptions, ReqId),
Element (m_assignmentCostMatrixes, ReqId)));
---------------------------
-- Service functionality --
@@ -80,7 +125,10 @@ package Assignment_Tree_Branch_Bound with SPARK_Mode is
State : in out Assignment_Tree_Branch_Bound_State;
Areq : UniqueAutomationRequest)
with
Pre => not Contains (State.m_uniqueAutomationRequests, Areq.RequestID);
Pre =>
not Contains (State.m_uniqueAutomationRequests, Areq.RequestID)
and then
not Contains (State.m_assignmentCostMatrixes, Areq.RequestID);
procedure Handle_Task_Plan_Options
(Mailbox : in out Assignment_Tree_Branch_Bound_Mailbox;
@@ -90,12 +138,20 @@ package Assignment_Tree_Branch_Bound with SPARK_Mode is
with
Pre =>
(for all TaskOption of Options.Options =>
(TaskOption.Cost >= 0
and then Options.TaskID = TaskOption.TaskID))
(TaskOption.Cost >= 0 and then Options.TaskID = TaskOption.TaskID))
and then not Contains (State.m_assignmentCostMatrixes, Options.CorrespondingAutomationRequestID)
and then
(not Contains (State.m_taskPlanOptions, Options.CorrespondingAutomationRequestID)
or else
not Has_Key (Element (State.m_taskPlanOptions, Options.CorrespondingAutomationRequestID), Options.TaskID));
(not Contains (State.m_taskPlanOptions, Options.CorrespondingAutomationRequestID)
or else
not Has_Key (Element (State.m_taskPlanOptions, Options.CorrespondingAutomationRequestID), Options.TaskID))
and then Contains (State.m_uniqueAutomationRequests, Options.CorrespondingAutomationRequestID)
and then
(for all Option of Options.Options =>
(for all EntityId of Option.EligibleEntities =>
Contains (Element (State.m_uniqueAutomationRequests, Options.CorrespondingAutomationRequestID).EntityList,
TO_Sequences.First,
Last (Element (State.m_uniqueAutomationRequests, Options.CorrespondingAutomationRequestID).EntityList),
EntityId)));
procedure Handle_Assignment_Cost_Matrix
(Mailbox : in out Assignment_Tree_Branch_Bound_Mailbox;
@@ -104,7 +160,12 @@ package Assignment_Tree_Branch_Bound with SPARK_Mode is
Matrix : AssignmentCostMatrix)
with Pre =>
not Contains (State.m_assignmentCostMatrixes, Matrix.CorrespondingAutomationRequestID)
and then Valid_AssignmentCostMatrix (Matrix);
and then Valid_AssignmentCostMatrix (Matrix)
and then Contains (State.m_uniqueAutomationRequests, Matrix.CorrespondingAutomationRequestID)
and then Contains (State.m_taskPlanOptions, Matrix.CorrespondingAutomationRequestID)
and then All_Travels_In_CostMatrix (Element (State.m_uniqueAutomationRequests, Matrix.CorrespondingAutomationRequestID),
Element (State.m_taskPlanOptions, Matrix.CorrespondingAutomationRequestID),
Matrix);
procedure Check_Assignment_Ready
(Mailbox : in out Assignment_Tree_Branch_Bound_Mailbox;
@@ -144,7 +205,11 @@ package Assignment_Tree_Branch_Bound with SPARK_Mode is
Has_Key (TaskPlanOptions_Map, TaskId))
and then
(for all Id of TaskPlanOptions_Map =>
(for all TaskOption of Get (TaskPlanOptions_Map, Id).Options => TaskOption.TaskID = Id));
(for all TaskOption of Get (TaskPlanOptions_Map, Id).Options => TaskOption.TaskID = Id))
and then
All_Travels_In_CostMatrix (Automation_Request, TaskPlanOptions_Map, Assignment_Cost_Matrix)
and then
All_EligibleEntities_In_EntityList (Automation_Request, TaskPlanOptions_Map);
-- Returns the assignment that minimizes the cost.
private
@@ -165,4 +230,68 @@ private
return Boolean
is
(for all TOC of Assignment_Cost_Matrix.CostMatrix => TOC.TimeToGo >= 0);
function Travel_In_CostMatrix
(VehicleId : Int64;
DestOption : TaskOption;
Assignment_Cost_Matrix : AssignmentCostMatrix)
return Boolean
is
(for some TOC of Assignment_Cost_Matrix.CostMatrix =>
(VehicleId = TOC.VehicleID
and then 0 = TOC.InitialTaskID
and then 0 = TOC.InitialTaskOption
and then DestOption.TaskID = TOC.DestinationTaskID
and then DestOption.OptionID = TOC.DestinationTaskOption));
function Travel_In_CostMatrix
(VehicleId : Int64;
InitOption, DestOption : TaskOption;
Assignment_Cost_Matrix : AssignmentCostMatrix)
return Boolean
is
(for some TOC of Assignment_Cost_Matrix.CostMatrix =>
(VehicleId = TOC.VehicleID
and then InitOption.TaskID = TOC.InitialTaskID
and then InitOption.OptionID = TOC.InitialTaskOption
and then DestOption.TaskID = TOC.DestinationTaskID
and then DestOption.OptionID = TOC.DestinationTaskOption));
function Is_Eligible (Request : UniqueAutomationRequest; Option : TaskOption; VehicleId : Int64) return Boolean is
(Contains (Request.EntityList, TO_Sequences.First, Last (Request.EntityList), VehicleId)
and then
(if Length (Option.EligibleEntities) > 0 then Contains (Option.EligibleEntities, TO_Sequences.First, Last (Option.EligibleEntities), VehicleId)));
function All_Travels_In_CostMatrix
(Request : UniqueAutomationRequest;
TaskPlanOptions_Map : Int64_TPO_Map;
Matrix : AssignmentCostMatrix)
return Boolean
is
(for all VehicleId of Request.EntityList =>
(for all TaskId_1 of TaskPlanOptions_Map =>
(for all Option_1 of Get (TaskPlanOptions_Map, TaskId_1).Options =>
(if Is_Eligible (Request, Option_1, VehicleId)
then
Travel_In_CostMatrix (VehicleId, Option_1, Matrix)
and then
(for all TaskId_2 of TaskPlanOptions_Map =>
(for all Option_2 of Get (TaskPlanOptions_Map, TaskId_2).Options =>
(if Option_1 /= Option_2 and then Is_Eligible (Request, Option_2, VehicleId)
then
Travel_In_CostMatrix (VehicleId,
Option_1,
Option_2,
Matrix))))))));
function All_EligibleEntities_In_EntityList
(Request : UniqueAutomationRequest;
TaskPlanOptions_Map : Int64_TPO_Map)
return Boolean
is
(for all TaskId of TaskPlanOptions_Map =>
(for all Option of Get (TaskPlanOptions_Map, TaskId).Options =>
(for all EntityId of Option.EligibleEntities =>
Contains (Request.EntityList, TO_Sequences.First, Last (Request.EntityList), EntityId))));
end Assignment_Tree_Branch_Bound;