using System.Threading; using FluentAssertions; using FsCheck; using FsCheck.Xunit; using SchotzIadKmTracker.Api.Services; using SchotzIadKmTracker.Api.Services.Exceptions; using Xunit; namespace SchotzIadKmTracker.Tests.PrecisionDistance; /// /// Tests de propriétés (FsCheck.Xunit, >= 100 itérations) du service de précision des /// distances (feature precision-distances-km), couvrant les Correctness Properties /// 1, 4 et 5 de la conception. /// public class PrecisionDistanceServiceProperties { // --- Générateurs contraints à l'espace d'entrée pertinent ------------------ /// Distances brutes positives et raisonnables (0 exclu, jusqu'à 100 000 km). private static Arbitrary DistancePositiveArb() { var g = from entier in Gen.Choose(1, 100_000_00) select entier / 100m; // pas de 0.01 km, jusqu'à 100 000.00 km return Arb.From(g); } /// Précisions valides : 0, 1 ou 2. private static Arbitrary PrecisionValideArb() => Arb.From(Gen.Elements(0, 1, 2)); /// Entiers arbitraires, y compris hors de {0, 1, 2} (négatifs et > 2). private static Arbitrary EntierArbitraireArb() => Arb.From(Gen.Choose(-1000, 1000)); // --------------------------------------------------------------------------- // Feature: precision-distances-km, Property 1: Arrondi supérieur exact et jamais inférieur à la distance brute // Pour toute distance brute positive et toute précision valide (0,1,2), ArrondirDistance // retourne une valeur >= distance brute, et le résultat × 10^precision est un entier. // Validates: Requirements 3.1, 3.2, 3.3, 3.4, 3.5 [Property(MaxTest = 100)] public Property P1_Arrondi_superieur_exact_et_jamais_inferieur() { return Prop.ForAll(DistancePositiveArb(), PrecisionValideArb(), (distance, precision) => { using var h = new PrecisionDistanceTestHarness(); var resultat = h.PrecisionDistanceService.ArrondirDistance(distance, precision); // Jamais inférieur à la distance brute. resultat.Should().BeGreaterThanOrEqualTo(distance); // Le résultat × 10^precision est un entier exact (multiple du pas de précision). var facteur = (decimal)Math.Pow(10, precision); var mis = resultat * facteur; mis.Should().Be(Math.Round(mis, 0)); }); } // Feature: precision-distances-km, Property 4: Validation stricte de la précision // Pour tout entier, DefinirAsync accepte et persiste si et seulement si la valeur ∈ {0,1,2} ; // sinon exception levée et valeur précédente inchangée. // Validates: Requirements 1.6 [Property(MaxTest = 100)] public Property P4_Validation_stricte_de_la_precision() { return Prop.ForAll(EntierArbitraireArb(), valeur => { using var h = new PrecisionDistanceTestHarness(); // Valeur initiale connue, différente des valeurs de test invalides typiques. var precedente = h.PrecisionDistanceService.DefinirAsync(1, CancellationToken.None) .GetAwaiter().GetResult(); if (valeur is 0 or 1 or 2) { var resultat = h.PrecisionDistanceService.DefinirAsync(valeur, CancellationToken.None) .GetAwaiter().GetResult(); resultat.Should().Be(valeur); h.PrecisionDistanceService.ObtenirAsync(CancellationToken.None) .GetAwaiter().GetResult().Should().Be(valeur); } else { Func action = () => h.PrecisionDistanceService.DefinirAsync(valeur, CancellationToken.None); action.Should().ThrowAsync().GetAwaiter().GetResult(); // La valeur précédemment persistée (1) reste inchangée. h.PrecisionDistanceService.ObtenirAsync(CancellationToken.None) .GetAwaiter().GetResult().Should().Be(precedente); } }); } // Feature: precision-distances-km, Property 5: Invariance de la distance brute stockée // Un changement de Precision_Distance ne modifie jamais Trajet.Distance en base. // Validates: Requirements 1.5, 1.8 [Property(MaxTest = 100)] public Property P5_Invariance_de_la_distance_brute_stockee() { return Prop.ForAll(DistancePositiveArb(), PrecisionValideArb(), PrecisionValideArb(), (distanceBrute, premierePrecision, deuxiemePrecision) => { using var h = new PrecisionDistanceTestHarness(); var vehiculeId = h.AjouterVehicule(); var trajetId = h.AjouterTrajet(vehiculeId, new DateOnly(2025, 6, 15), distanceBrute); // Deux changements successifs de précision (valides). h.PrecisionDistanceService.DefinirAsync(premierePrecision, CancellationToken.None) .GetAwaiter().GetResult(); h.PrecisionDistanceService.DefinirAsync(deuxiemePrecision, CancellationToken.None) .GetAwaiter().GetResult(); // La distance brute stockée en base reste strictement inchangée. var trajet = h.Context.Trajets.Single(t => t.Id == trajetId); trajet.Distance.Should().Be(distanceBrute); }); } }