namespace SpecExplorer5.TestSuite {
    using System;
    using System.Collections.Generic;
    using System.Text;
    using System.Reflection;
    using Microsoft.SpecExplorer.Runtime.Testing;
    using Microsoft.VisualStudio.TestTools.UnitTesting;

    [System.CodeDom.Compiler.GeneratedCodeAttribute("Spec Explorer", "3.5.3130.0")]
    [Microsoft.VisualStudio.TestTools.UnitTesting.TestClassAttribute()]
    public partial class AccumulatorTestSuite : VsTestClassBase {
        
        public AccumulatorTestSuite() {
            this.SetSwitch("ProceedControlTimeout", "100");
            this.SetSwitch("QuiescenceTimeout", "30000");
        }
        
        #region Test Initialization and Cleanup
        [Microsoft.VisualStudio.TestTools.UnitTesting.TestInitializeAttribute()]
        public virtual void TestInitialize() {
            this.InitializeTestManager();
        }
        
        [Microsoft.VisualStudio.TestTools.UnitTesting.TestCleanupAttribute()]
        public virtual void TestCleanup() {
            this.CleanupTestManager();
        }
        #endregion
        
        #region Test Starting in S0
        [Microsoft.VisualStudio.TestTools.UnitTesting.TestMethodAttribute()]
        public void AccumulatorTestSuiteS0() {
            this.Manager.BeginTest("AccumulatorTestSuiteS0");
            this.Manager.Comment("reaching state \'S0\'");
            this.Manager.Comment("executing step \'call Add(2)\'");
            SpecExplorer5.Sample.Accumulator.Add(2);
            this.Manager.Comment("reaching state \'S1\'");
            this.Manager.Comment("checking step \'return Add\'");
            this.Manager.Comment("reaching state \'S8\'");
            this.Manager.Comment("executing step \'call Add(2)\'");
            SpecExplorer5.Sample.Accumulator.Add(2);
            this.Manager.Comment("reaching state \'S12\'");
            this.Manager.Comment("checking step \'return Add\'");
            this.Manager.Comment("reaching state \'S16\'");
            int temp0;
            this.Manager.Comment("executing step \'call ReadAndReset()\'");
            temp0 = SpecExplorer5.Sample.Accumulator.ReadAndReset();
            this.Manager.Comment("reaching state \'S20\'");
            this.Manager.Comment("checking step \'return ReadAndReset/4\'");
            TestManagerHelpers.AssertAreEqual<int>(this.Manager, 4, temp0, "return of ReadAndReset, state S20");
            this.Manager.Comment("reaching state \'S24\'");
            this.Manager.EndTest();
        }
        #endregion
        
        #region Test Starting in S2
        [Microsoft.VisualStudio.TestTools.UnitTesting.TestMethodAttribute()]
        public void AccumulatorTestSuiteS2() {
            this.Manager.BeginTest("AccumulatorTestSuiteS2");
            this.Manager.Comment("reaching state \'S2\'");
            this.Manager.Comment("executing step \'call Add(2)\'");
            SpecExplorer5.Sample.Accumulator.Add(2);
            this.Manager.Comment("reaching state \'S3\'");
            this.Manager.Comment("checking step \'return Add\'");
            this.Manager.Comment("reaching state \'S9\'");
            this.Manager.Comment("executing step \'call Add(1)\'");
            SpecExplorer5.Sample.Accumulator.Add(1);
            this.Manager.Comment("reaching state \'S13\'");
            this.Manager.Comment("checking step \'return Add\'");
            this.Manager.Comment("reaching state \'S17\'");
            int temp1;
            this.Manager.Comment("executing step \'call ReadAndReset()\'");
            temp1 = SpecExplorer5.Sample.Accumulator.ReadAndReset();
            this.Manager.Comment("reaching state \'S21\'");
            this.Manager.Comment("checking step \'return ReadAndReset/3\'");
            TestManagerHelpers.AssertAreEqual<int>(this.Manager, 3, temp1, "return of ReadAndReset, state S21");
            this.Manager.Comment("reaching state \'S25\'");
            this.Manager.EndTest();
        }
        #endregion
        
        #region Test Starting in S4
        [Microsoft.VisualStudio.TestTools.UnitTesting.TestMethodAttribute()]
        public void AccumulatorTestSuiteS4() {
            this.Manager.BeginTest("AccumulatorTestSuiteS4");
            this.Manager.Comment("reaching state \'S4\'");
            this.Manager.Comment("executing step \'call Add(1)\'");
            SpecExplorer5.Sample.Accumulator.Add(1);
            this.Manager.Comment("reaching state \'S5\'");
            this.Manager.Comment("checking step \'return Add\'");
            this.Manager.Comment("reaching state \'S10\'");
            this.Manager.Comment("executing step \'call Add(2)\'");
            SpecExplorer5.Sample.Accumulator.Add(2);
            this.Manager.Comment("reaching state \'S14\'");
            this.Manager.Comment("checking step \'return Add\'");
            this.Manager.Comment("reaching state \'S18\'");
            int temp2;
            this.Manager.Comment("executing step \'call ReadAndReset()\'");
            temp2 = SpecExplorer5.Sample.Accumulator.ReadAndReset();
            this.Manager.Comment("reaching state \'S22\'");
            this.Manager.Comment("checking step \'return ReadAndReset/3\'");
            TestManagerHelpers.AssertAreEqual<int>(this.Manager, 3, temp2, "return of ReadAndReset, state S22");
            this.Manager.Comment("reaching state \'S26\'");
            this.Manager.EndTest();
        }
        #endregion
        
        #region Test Starting in S6
        [Microsoft.VisualStudio.TestTools.UnitTesting.TestMethodAttribute()]
        public void AccumulatorTestSuiteS6() {
            this.Manager.BeginTest("AccumulatorTestSuiteS6");
            this.Manager.Comment("reaching state \'S6\'");
            this.Manager.Comment("executing step \'call Add(1)\'");
            SpecExplorer5.Sample.Accumulator.Add(1);
            this.Manager.Comment("reaching state \'S7\'");
            this.Manager.Comment("checking step \'return Add\'");
            this.Manager.Comment("reaching state \'S11\'");
            this.Manager.Comment("executing step \'call Add(1)\'");
            SpecExplorer5.Sample.Accumulator.Add(1);
            this.Manager.Comment("reaching state \'S15\'");
            this.Manager.Comment("checking step \'return Add\'");
            this.Manager.Comment("reaching state \'S19\'");
            int temp3;
            this.Manager.Comment("executing step \'call ReadAndReset()\'");
            temp3 = SpecExplorer5.Sample.Accumulator.ReadAndReset();
            this.Manager.Comment("reaching state \'S23\'");
            this.Manager.Comment("checking step \'return ReadAndReset/2\'");
            TestManagerHelpers.AssertAreEqual<int>(this.Manager, 2, temp3, "return of ReadAndReset, state S23");
            this.Manager.Comment("reaching state \'S27\'");
            this.Manager.EndTest();
        }
        #endregion
    }
}