Compare commits

..

9 Commits

Author SHA1 Message Date
Nina Chlóe Kassandra Reiß 4fa5426a15 Add flake
Alire installation and checkup / build (ubuntu-20.04) (push) Failing after 5m45s
2026-07-18 21:35:06 +02:00
Nina Chlóe Kassandra Reiß e1f7097bc3 Warshall algorithm reference 2026-07-18 21:34:45 +02:00
Nina Chlóe Kassandra Reiß 64cfecef9a Add distance calculation based on haversine
Alire installation and checkup / build (ubuntu-20.04) (push) Failing after 4m0s
2026-06-15 05:38:52 +02:00
Nina Chlóe Kassandra Reiß 4af251007f Default packages
Alire installation and checkup / build (ubuntu-20.04) (push) Failing after 4m3s
2026-06-14 22:37:02 +02:00
Nina Chlóe Kassandra Reiß cdf1ca655d Add gnatprove as dependency
Alire installation and checkup / build (ubuntu-20.04) (push) Failing after 4m32s
2026-06-14 22:00:40 +02:00
Nina Chlóe Kassandra Reiß 4cb0066d0e Retry after local verification
Alire installation and checkup / build (ubuntu-20.04) (push) Failing after 4m39s
2026-06-11 16:23:39 +02:00
Nina Chlóe Kassandra Reiß 6ad68af041 Refresh alire package index
Alire installation and checkup / build (ubuntu-20.04) (push) Failing after 41s
2026-06-11 15:59:47 +02:00
Nina Chlóe Kassandra Reiß 5f4923a127 Install gnatprove systemwide
Alire installation and checkup / build (ubuntu-20.04) (push) Failing after 40s
2026-06-11 15:56:00 +02:00
Nina Chlóe Kassandra Reiß 32633ed60b Shipping gnatprove doesn't work 2026-06-11 15:55:05 +02:00
7 changed files with 153 additions and 1 deletions
+2
View File
@@ -32,6 +32,8 @@ jobs:
mv alr /bin/alr
fi
chmod +x /bin/alr
/bin/alr index --update-all
/bin/alr install gnatprove
- name: build project
run: |
+30
View File
@@ -0,0 +1,30 @@
#!/usr/bin/env bash
"""
File: adj2con.py
Author: Nina Chloe Kassandra Reiß <nina.reiss@nickr.eu>
Created on: Sa 18. Jul 11:30:03 CEST 2026
Description: Turn adjacency matrices into boolean connectivity matrix
"""
adjacency = [[1, 0, 1, 0, 0, 0], [0, 0, 0, 0, 1, 0], [1, 0, 0, 0, 0, 0],
[0, 0, 0, 0, 1, 0], [0, 0, 0, 1, 0, 0], [0, 0, 0, 1, 1, 0]]
def warshall(adj):
n = len(adj)
# Kopie erzeugen
R = [row[:] for row in adj]
# Jeder Knoten ist von sich selbst erreichbar
for i in range(n):
R[i][i] = 1
for k in range(n):
for i in range(n):
for j in range(n):
R[i][j] = R[i][j] or (R[i][k] and R[k][j])
return R
print(warshall(adjacency))
+61
View File
@@ -0,0 +1,61 @@
{
description = "Ada development environment with Alire";
inputs = {
nixpkgs.url = "github:NixOS/nixpkgs/nixos-26.05";
flake-utils.url = "github:numtide/flake-utils";
};
outputs =
{
self,
nixpkgs,
flake-utils,
}:
flake-utils.lib.eachDefaultSystem (
system:
let
pkgs = import nixpkgs {
inherit system;
};
in
{
devShells.default = pkgs.mkShell {
packages = with pkgs; [
# Ada
gnat
gprbuild
alire
# Toolchain
gcc
binutils
# Build Tools
gnumake
cmake
pkg-config
# Debugging
gdb
# Utilities
git
which
file
];
shellHook = ''
export ADA_PROJECT_PATH="$PWD''${ADA_PROJECT_PATH:+:$ADA_PROJECT_PATH}"
echo "Ada + Alire development shell"
echo "--------------------------------"
command -v alr >/dev/null && alr --version
command -v gnat >/dev/null && gnat --version | head -n1
command -v gprbuild >/dev/null && gprbuild --version | head -n1
'';
};
}
);
}
+37
View File
@@ -1,3 +1,5 @@
with Ada.Numerics.Elementary_Functions; use Ada.Numerics.Elementary_Functions;
package body Grl.Coordinates is
function To_DD (DM_Base : Coordinate) return Coordinate is
@@ -37,4 +39,39 @@ package body Grl.Coordinates is
return DD_Target;
end To_DD;
function Plane_Distance (Origin, Destination : Coordinate) return H is
Heuristic : H;
A : H;
DD_Origin : constant Coordinate := To_DD (Origin);
DD_Destination : constant Coordinate := To_DD (Destination);
Earth_Radius : constant H := 6_371_000.0; -- M
Delta_Phi : constant H := -- Latitude difference
H (DD_Destination.DD.Latitude - DD_Origin.DD.Latitude);
Delta_Lambda : constant H := -- Longitude difference
H (DD_Destination.DD.Longitude - DD_Origin.DD.Longitude);
-- @name Hav
-- @return Float
-- @parameter Theta:Float
-- @variable Fraction : Float
-- @description Compute Haversine function.
function Hav (Theta : H) return Float is
Fraction : Float;
begin
Fraction := Float (Theta) / 2.0;
return Sin (Fraction)**2;
end Hav;
begin
A :=
H (Hav (Delta_Phi) +
Cos (Float (DD_Origin.DD.Latitude)) *
Cos (Float (DD_Destination.DD.Latitude)) * Hav (Delta_Lambda));
-- Haversine formula
Heuristic := Earth_Radius * H (2.0 * Arcsin (Sqrt (Float (A))));
return Heuristic;
end Plane_Distance;
end Grl.Coordinates;
+20
View File
@@ -1,3 +1,6 @@
generic
type Meta is private;
type H is digits <>;
package Grl.Coordinates with
SPARK_Mode => On
is
@@ -92,6 +95,15 @@ is
end case;
end record;
-- ------------------------ --
-- Location Type Definition --
-- ------------------------ --
type Location is record
Where : Coordinate;
Heuristic : H;
Data : Meta;
end record;
-- ---------------------------- --
-- Converter / helper functions --
-- ---------------------------- --
@@ -106,4 +118,12 @@ is
(DM_Base.Form = DD) or else (DM_Base.Form = DMS)
or else (DM_Base.Form = DDM);
-- @name Plane_Distance
-- @return H
-- @parameter Origin:Coordinate
-- @parameter Destination:Coordinate
-- @variable Heuristic : H
-- @description Calculate heuristic between coordinates.
function Plane_Distance (Origin, Destination : Coordinate) return H;
end Grl.Coordinates;
+3
View File
@@ -0,0 +1,3 @@
with Grl.Coordinates;
package Grl.Default is new Grl.Coordinates (Meta => Natural, H => Float);
-1
View File
@@ -1,3 +1,2 @@
package Grl is
end Grl;