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);
});
}
}