using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Pex.Framework;
using Microsoft.VisualStudio.TestTools.UnitTesting;

namespace MockObjectSample
{
    public interface IFileSystem
    {
        bool CreateFile(string s);
        bool DeleteFile(string s);
        bool FileExists(string s);
    }

    public class MFileSystem : IFileSystem
    {
        //if there is an entry in Files, we are certain that
        //file indeed exists (its mapped bool is true)
        //or does not exist (its mapped bool is false)
        Dictionary<string, bool> Files = new Dictionary<string, bool>();

        public bool CreateFile(string s)
        //return true when the file is created or already exists
        {
            PexAssert.IsTrue(s != null);
            bool fileExists;
            bool availableInFiles = Files.TryGetValue(s, out fileExists);
            if (availableInFiles)
            {
                return fileExists;//note that here if a file with the same name, already exists, we return true
            }
            else
            {
                var call = PexChoose.FromCall(this);
                bool result = call.ChooseResult<bool>();
                if (result)
                    Files.Add(s, true);
                return result;
            }
        }

        public bool DeleteFile(string s)
        //return true when the file exists and is deleted
        {
            if (s == null)
                return false;
            bool fileExists;
            bool availableInFiles = Files.TryGetValue(s, out fileExists);
            if (availableInFiles)
            {
                Files.Remove(s);
                Files.Add(s, false);
                return true;     
            }
            else
            {
                Files.Add(s, false);
                var call = PexChoose.FromCall(this);
                bool result = call.ChooseResult<bool>();
                return result;
            }                               
        }

        public bool FileExists(string s)
        //return true when the file exists
        {
            if (s == null)
                return false;

            bool fileExists;
            bool availableInFiles = Files.TryGetValue(s, out fileExists);
            if (availableInFiles)
            {
                return fileExists;
            }
            else 
            {
                var call = PexChoose.FromCall(this);
                bool result = call.ChooseResult<bool>();
                Files.Add(s, result);
                return result;               
            }
        }
    }

    [PexClass]
    public partial class MockObjectSample
    {
        [PexMethod]
        public void TestFileSystem(IFileSystem file,
                    string s1, string s2, string s3,
                    int count)
        {
            PexAssume.IsTrue(s1 != null);
            PexAssume.IsTrue(file != null);
            int i = 0;
            for (int j = 0; j < count; j++)
            {
                bool successInCreatingFile = file.CreateFile(s1);
                if (successInCreatingFile)          
                    i++;
                else
                    i--;

                bool successInDeletingFile = file.DeleteFile(s2);
                if (successInDeletingFile)
                    i++;
                else
                    i--;

                bool fileExists = file.FileExists(s3);
                if (fileExists)               
                    i++;
                else
                    i--;
            }
        }
    }
}