using System;
using NUnit.Framework;
using STVrogue.TestInfrastructure;
using static STVrogue.TestInfrastructure.TemporalProperty<int> ;

namespace NUnitTests
{
    class IntSequence : GamePlay<int>
    {
        
        int[] sequence;
            
        public IntSequence(params int[] data) {  sequence = data; }
        public void ResetReplayState() { }
        
        public string ReplayId()
        {
            string s = "";
            for(int k=0 ; k<sequence.Length; k++)
            {
                if (k > 0) s += ",";
                s += sequence[k];
            }
            return $"seq: {s}";
        }

        public Judgement Satisfies(TemporalProperty<int> phi)
        {
            phi.Reset();
            Judgement j = Judgement.Inconclusive;
            foreach (var x in sequence)
            {
                j = phi.EvaluateNextState(x);
            }

            return j;
        }
    }
    
    [TestFixture]
    public class TestTemporalProperties
    {
        [Test]
        public void test1()
        {
            var seq1 = new IntSequence(0, 1, 2, 3, 4);
            Assert.AreEqual(Judgement.Valid, seq1.Satisfies(Always(x => x >= 0))) ;
            Assert.AreEqual(Judgement.Invalid, seq1.Satisfies(Always(x => x != 2))) ;
            Assert.AreEqual(Judgement.Valid, seq1.Satisfies(Eventually(x => x == 3))) ;
            Assert.AreEqual(Judgement.Invalid, seq1.Satisfies(Eventually(x => x < 0))) ;
            Assert.AreEqual(Judgement.Valid, seq1.Satisfies(
                    And(Always(x => x >= 0),
                           Eventually(x => x==4)))
                    );
            Assert.AreEqual(Judgement.Valid, seq1.Satisfies(
                Or(Always(x => x < 0),
                      Eventually(x => x==4)))
            );
        }

        [Test]
        public void testChangePreds()
        {
            var seq1 = new IntSequence(0, 1, 2, 3, 4);
            Assert.AreEqual(Judgement.Valid, 
                seq1.Satisfies(Always(x => 2*x,  (x0,x) =>
                {    Console.WriteLine($">> x0={x0}, x={x}");
                     return x == 2+x0;
                }))) ;
            Assert.AreEqual(Judgement.Invalid, 
                seq1.Satisfies(Eventually(x => 2*x,  (x0,x) => x>0 && x == x0))) ;
            
            var seq2 = new IntSequence(0, 1);
            Assert.AreEqual(Judgement.Valid, 
                seq2.Satisfies(Always(x => 2*x,  (x0,x) => x == x0+2))) ;
            
            var seq3 = new IntSequence(0);
            Assert.AreEqual(Judgement.Inconclusive, 
                seq3.Satisfies(Always(x => 2*x,  (x0,x) => x == x0+2))) ;
        }

        [Test]
        public void test3()
        {
            GamePlay<int>[] seqs =
            {
                new IntSequence(0, 1, 2, 3, 4),
                new IntSequence(1, 1, 2, 3, 3),
                new IntSequence(4, 3, 2, 1, 0)
            };
            Assert.IsTrue(Always(x => 0 <= x && x <= 4).SatisfiedByAll(seqs));
            Assert.IsFalse(Eventually(x => x == 4).SatisfiedByAll(seqs));
            Assert.IsTrue(Eventually(x => x == 4).SatisfiedBySome(seqs));
            Assert.AreEqual(Judgement.Valid,
                Eventually(x => x == 4).SatisfiedByGroup(Eventually(x => x == 0), seqs));
            Assert.AreEqual(Judgement.Inconclusive,
                Eventually(x => x == 4).SatisfiedByGroup(Eventually(x => x < 0), seqs));
        }
    }
}