using System;
using STVrogue;
using STVrogue.GameLogic;
using STVrogue.TestInfrastructure;
using STVrogue.Utils;
using static STVrogue.TestInfrastructure.TemporalProperty<STVrogue.GameLogic.Game>;

namespace TestInstrumentedSTV
{
    class Program
    {
        
        /// <summary>
        /// Demonstrating the use of replay-console to replay a recorded play. In the
        /// example, the recorded play will be explicitly specified as a list of inputs.
        /// The play is then runs several times to check temporal-properties.
        ///
        /// <para></para> You need a working implementation of <see cref="ReplayGameConsole"/>.
        /// </summary>
        /// <param name="args"></param>
        static void Main(string[] args)
        {
            STVLogger.Log(">>> Test");
            // (1) Create a dungeon according to a configuration file:
            GameConfiguration conf = new GameConfiguration("rogueconfig.txt");
            Game game = new Game(conf);
            STVLogger.Log(">>> config: \n" + conf.ToString());
            // (2) attach a replay-console (you need a working implementation of ReplayGameConsole):
            ReplayGameConsole replayConsole = new ReplayGameConsole();
            game.GameConsole = replayConsole;
            // add this input sequence to the replau-console: attack,attack,flee,quit:
            replayConsole.SeedInputs("a","a","f","q");
            // (3) create a runner for the game:
            var runner = new GameRunner(game);
            // (4a) new we can replay the sequence:
            runner.Run();
            // (4b) we can also replay the sequence to check correctness properties. Three
            // examples are shown below:
            Judgement j = runner.Satisfies(Always(gamestate => gamestate.Player.Hp == 100));
            STVLogger.Log($">>> Judgement-1: {j}");
            //STVLogger.Log($"--- #msgIn={((InstrumentedGameConsole)game.GameConsole).MsgIn.Count}");
            j = runner.Satisfies(Eventually(gamestate => gamestate.Player.Hp < 100));
            STVLogger.Log($">>> Judgement-2: {j}");
            j = runner.Satisfies(Always(gamestate => gamestate.Player.Hp < 100));
            STVLogger.Log($">>> Judgement-3: {j}");
        }
    }
}