SchotzIAD/backend/SchotzIadKmTracker.Tests/PrecisionDistance/MontantPrevisionnelProperties.cs

using System.Threading;
using FluentAssertions;
using FsCheck;
using FsCheck.Xunit;
using Xunit;

namespace SchotzIadKmTracker.Tests.PrecisionDistance;

/// <summary>
/// Tests de propriétés (FsCheck.Xunit, >= 100 itérations) du calcul prévisionnel
/// (feature precision-distances-km), couvrant les Correctness Properties 6 et 7 de la
/// conception (<see cref="MontantRegleService.GetMontantPrevisionnelAsync"/>).
/// </summary>
public class MontantPrevisionnelProperties
{
    private const int Annee = 2025;
    private const int PuissanceFiscale = 5;

    /// <summary>Distances brutes positives et raisonnables (0 exclu, jusqu'à 500 km par trajet).</summary>
    private static Arbitrary<decimal> DistancePositiveArb()
    {
        var g =
            from entier in Gen.Choose(1, 50_000)
            select entier / 100m; // pas de 0.01 km, jusqu'à 500.00 km

        return Arb.From(g);
    }

    private static Arbitrary<int> PrecisionValideArb() => Arb.From(Gen.Elements(0, 1, 2));

    /// <summary>Mois autre que le mois M passé en paramètre (1..12, différent de M).</summary>
    private static Gen<int> AutreMoisGen(int mois) =>
        Gen.Elements(Enumerable.Range(1, 12).Where(m => m != mois).ToArray());

    // Feature: precision-distances-km, Property 6: Montant_Previsionnel_Mensuel dépend uniquement du mois affiché
    // Pour tout mois M, le montant mensuel ne change pas si on modifie les distances d'un autre
    // mois, tant que le cumul annuel reste dans la même tranche de barème.
    // Validates: Requirements 7.1, 7.2
    [Property(MaxTest = 100)]
    public Property P6_Montant_previsionnel_mensuel_depend_uniquement_du_mois_affiche()
    {
        var entreesArb = Arb.From(
            from mois in Gen.Choose(1, 12)
            from distanceMois in DistancePositiveArb().Generator
            from distanceAutre in DistancePositiveArb().Generator
            from precision in PrecisionValideArb().Generator
            select (mois, distanceMois, distanceAutre, precision));

        return Prop.ForAll(entreesArb, entree =>
            {
                var (moisAffiche, distanceMoisAffiche, distanceAutreMoisInitiale, precision) = entree;
                using var h = new PrecisionDistanceTestHarness();

                h.PrecisionDistanceService.DefinirAsync(precision, CancellationToken.None)
                    .GetAwaiter().GetResult();

                // Une seule tranche illimitée : garantit que le cumul annuel reste TOUJOURS
                // dans la même tranche, quelle que soit la distance de l'autre mois modifiée.
                h.AjouterTrancheBaremeUnique(Annee, PuissanceFiscale, coefficient: 0.35m, baseFixe: 0m);

                var vehiculeId = h.AjouterVehicule(PuissanceFiscale);
                var autreMois = AutreMoisGen(moisAffiche).Sample(0, 1).First();

                h.AjouterTrajet(vehiculeId, new DateOnly(Annee, moisAffiche, 1), distanceMoisAffiche);
                var trajetAutreMoisId = h.AjouterTrajet(
                    vehiculeId, new DateOnly(Annee, autreMois, 1), distanceAutreMoisInitiale, position: 2m);

                var avant = h.MontantRegleService
                    .GetMontantPrevisionnelAsync(Annee, moisAffiche, vehiculeId, CancellationToken.None)
                    .GetAwaiter().GetResult();

                // Modification de la distance de l'AUTRE mois (le mois affiché n'est jamais touché).
                var trajetAutreMois = h.Context.Trajets.Single(t => t.Id == trajetAutreMoisId);
                trajetAutreMois.Distance = distanceAutreMoisInitiale + 10m;
                h.Context.SaveChanges();

                var apres = h.MontantRegleService
                    .GetMontantPrevisionnelAsync(Annee, moisAffiche, vehiculeId, CancellationToken.None)
                    .GetAwaiter().GetResult();

                // Le montant prévisionnel mensuel du mois affiché est inchangé (Requirement 7.1).
                apres.MontantPrevisionnelMensuel.Should().Be(avant.MontantPrevisionnelMensuel);
                apres.TotalMoisKm.Should().Be(avant.TotalMoisKm);
            });
    }

    // Feature: precision-distances-km, Property 7: Montant_Previsionnel_Annuel égal au barème plein sur le cumul
    // Pour tout Total_Annuel_Partiel arrondi, MontantPrevisionnelAnnuel == montant retourné par
    // CalculerMontantAsync appliqué à ce total, coefficient 1.00 (pas de minoration), arrondi 2 décimales.
    // Validates: Requirements 8.2, 8.5
    [Property(MaxTest = 100)]
    public Property P7_Montant_previsionnel_annuel_egal_au_bareme_plein_sur_le_cumul()
    {
        return Prop.ForAll(DistancePositiveArb(), PrecisionValideArb(), (distance, precision) =>
        {
            using var h = new PrecisionDistanceTestHarness();

            h.PrecisionDistanceService.DefinirAsync(precision, CancellationToken.None)
                .GetAwaiter().GetResult();

            h.AjouterTrancheBaremeUnique(Annee, PuissanceFiscale, coefficient: 0.35m, baseFixe: 10m);

            var vehiculeId = h.AjouterVehicule(PuissanceFiscale);
            h.AjouterTrajet(vehiculeId, new DateOnly(Annee, 6, 1), distance);

            var mois = 6;
            var resultat = h.MontantRegleService
                .GetMontantPrevisionnelAsync(Annee, mois, vehiculeId, CancellationToken.None)
                .GetAwaiter().GetResult();

            // Montant retourné par CalculerMontantAsync appliqué au même Total_Annuel_Partiel arrondi,
            // sans minoration (coefficient 1.00), arrondi à 2 décimales.
            var baremePlein = h.BaremeService
                .CalculerMontantAsync(Annee, PuissanceFiscale, resultat.TotalAnnuelPartielKm, CancellationToken.None)
                .GetAwaiter().GetResult();

            var montantAttendu = Math.Round(baremePlein.Montant, 2, MidpointRounding.AwayFromZero);

            resultat.MontantPrevisionnelAnnuel.Should().Be(montantAttendu);
        });
    }
}