Non-accepting state during repetition?

Question

Hi,

When I explored TwoInstanceConnectDisconnectScenario with repetition, I got into a non-accepting state. I'm unclear why it is the case.

I wonder whether we are allowed to use repetition operators from one machine to another machine.

// Test Scenario: Connect and Disconnect on Two instances

machine TwoInstancesConnectDisconnectScenario() : Main where ForExploration = false

{

   OneInstanceConnectDisconnectScenario(){2}

}

machine TwoInstancesConnectDisconnectProgram() : Main where ForExploration = true

{

    TwoInstancesConnectDisconnectScenario();exit || ModelProgram

}

machine TwoInstancesConnectDisconnectTestSuite() : Main where TestEnabled = true

{

    construct test cases where strategy = "shorttests" for TwoInstancesConnectDisconnectProgram()

}

// Test Scenario: Connect and Disconnect on One instance

machine OneInstanceConnectDisconnectScenario() : Main where ForExploration = false

{

   let SoftwareBusAdapterImpl conn in

   new conn.SoftwareBusAdapterImpl;conn.Create;(conn.Connect{2} ||| conn.Disconnect{2});conn.Destroy

}

machine OneInstanceConnectDisconnectProgram() : Main where ForExploration = true

{

   OneInstanceConnectDisconnectScenario();exit || ModelProgram

}

machine OneInstanceConnectDisconnectTestSuite() : Main where TestEnabled = true

{

    construct test cases where strategy = "shorttests" for OneInstanceConnectDisconnectProgram()

}

Thanks,

Dharma

Answer 1

Hi Dharma,

Your scenario looks good to me (and it ends in an accepting state) ...
So a problem might be in your model if you end in a non-accepting state:
* Maybe the scenario with {2} is not a valid one in your model.
  This is the case, if the last explored transition in machine "...Program" is not "exit".
* If the last transition is "exit", it seems that your [AcceptingStateCondition] is not true in this second repetition. So the model does not end in an accepting state here.
* If machine "...Program" is completely fine, but not machine "...TestSuite" you might have a problem with parameter expansion.

Maybe you have to post the model...

Answer 2

Hi,

Thanks a lot. I can post my model to you. Could you please send me your email?

Best regards,

Dharma

===========
FATAL ERROR: Object reference not set to an instance of an object.
stacktrace:
   at Microsoft.SpecExplorer.VS.SpecExplorerPackage.RecoverFromFatalError(Exception exception)
   at Microsoft.SpecExplorer.RecoverFromFatalErrorEventObserver.HandleEvent(ExplorerEvent e)
   at Microsoft.SpecExplorer.EventManager.HandleEvent(ExplorerEvent e)

involved exception: System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Xrt.State.ActiveState.IsExistential(Term term)
   at Microsoft.Xrt.Background.ConstraintStore.<>c__DisplayClass203.<GetContext>b__1fe(IntPtr t)
   at Microsoft.Xrt.Background.IsVarOrSelectorOnVarOrUnaryOperatorOnVar(IntPtr termPtr, Predicate`1 pred)
   at Microsoft.Xrt.Background.ConstraintStore.GetContext(Predicate`1 isExistential, Boolean removeMetaFunctions)
   at Microsoft.Xrt.Background.SaveNormalizedContext(Predicate`1 isExistential, Boolean removeMetaFunctions)
   at Microsoft.Xrt.State.ActiveState.<>c__DisplayClass2a.<Compress>b__29()
   at Microsoft.Xrt.State.HeapCompressor.Compress(Action collectOther)
   at Microsoft.Xrt.State.ActiveState.CompressHeaps(Action afterObjectHeapConsolidation)
   at Microsoft.Xrt.State.ActiveState.Compress(Boolean doConsolidate, TermSet& freed)
   at Microsoft.Xrt.State.ActiveState.Compress()
   at Microsoft.ActionMachines.RuleMachine.ActivationControlState.CanAssumeActionEquality(Action action, MachineState machineState, Nullable`1 demandedAction, MachineStep& resultStep)
   at Microsoft.ActionMachines.RuleMachine.ActivationControlState.<GetEntryStep>d__59.MoveNext()
   at Microsoft.ActionMachines.RuleMachine.ActivationControlState.<GetSteps>d__2a.MoveNext()
   at Microsoft.ActionMachines.DeclarationMachine.DeclarationControl.<GetSteps>d__d.MoveNext()
   at Microsoft.ActionMachines.ParallelMachine.ParallelControl.<GetCommonSteps>d__33.MoveNext()
   at Microsoft.ActionMachines.ParallelMachine.ParallelControl.<GetSteps>d__12.MoveNext()
   at Microsoft.ActionMachines.DeclarationMachine.DeclarationControl.<GetSteps>d__d.MoveNext()
   at Microsoft.ActionMachines.Explorer.OpenState.MoveNext()
   at Microsoft.ActionMachines.Explorer.OpenState..ctor(Nullable`1 incomingAction, MachineState state, OpenState previousState, Explorer explorer, Boolean isStart, Int32 pathBound)
   at Microsoft.ActionMachines.Explorer.Explore(IMachine machine)
   at Microsoft.ActionMachines.TransformationMachineProviderBase.Explore(ICompressedState initialState, IMachine machine)
   at Microsoft.ActionMachines.TransformationMachineBase.<GetInitialStates>d__0.MoveNext()
   at Microsoft.ActionMachines.DeclarationMachine.<GetInitialStates>d__0.MoveNext()
   at Microsoft.ActionMachines.Explorer.CreateInitialFrontier(IMachine machine, ICompressedState iniState)
   at Microsoft.ActionMachines.Explorer.Explore(IMachine machine)
   at Microsoft.SpecExplorer.ExploringOperator.Explore()
   at Microsoft.SpecExplorer.RemoteExplorer.Explore(IMachine machine, IConfiguration config)
   at Microsoft.SpecExplorer.RemoteExplorer.Work()
===========
===========
FATAL ERROR: Object reference not set to an instance of an object.
stacktrace:
   at Microsoft.SpecExplorer.VS.SpecExplorerPackage.RecoverFromFatalError(Exception exception)
   at Microsoft.SpecExplorer.RecoverFromFatalErrorEventObserver.HandleEvent(ExplorerEvent e)
   at Microsoft.SpecExplorer.EventManager.HandleEvent(ExplorerEvent e)

involved exception: System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Xrt.State.ActiveState.IsExistential(Term term)
   at Microsoft.Xrt.Background.ConstraintStore.<>c__DisplayClass203.<GetContext>b__1fe(IntPtr t)
   at Microsoft.Xrt.Background.IsVarOrSelectorOnVarOrUnaryOperatorOnVar(IntPtr termPtr, Predicate`1 pred)
   at Microsoft.Xrt.Background.ConstraintStore.GetContext(Predicate`1 isExistential, Boolean removeMetaFunctions)
   at Microsoft.Xrt.Background.SaveNormalizedContext(Predicate`1 isExistential, Boolean removeMetaFunctions)
   at Microsoft.Xrt.State.ActiveState.<>c__DisplayClass2a.<Compress>b__29()
   at Microsoft.Xrt.State.HeapCompressor.Compress(Action collectOther)
   at Microsoft.Xrt.State.ActiveState.CompressHeaps(Action afterObjectHeapConsolidation)
   at Microsoft.Xrt.State.ActiveState.Compress(Boolean doConsolidate, TermSet& freed)
   at Microsoft.Xrt.State.ActiveState.Compress()
   at Microsoft.ActionMachines.RuleMachine.ActivationControlState.CanAssumeActionEquality(Action action, MachineState machineState, Nullable`1 demandedAction, MachineStep& resultStep)
   at Microsoft.ActionMachines.RuleMachine.ActivationControlState.<GetEntryStep>d__59.MoveNext()
   at Microsoft.ActionMachines.RuleMachine.ActivationControlState.<GetSteps>d__2a.MoveNext()
   at Microsoft.ActionMachines.DeclarationMachine.DeclarationControl.<GetSteps>d__d.MoveNext()
   at Microsoft.ActionMachines.ParallelMachine.ParallelControl.<GetCommonSteps>d__33.MoveNext()
   at Microsoft.ActionMachines.ParallelMachine.ParallelControl.<GetSteps>d__12.MoveNext()
   at Microsoft.ActionMachines.DeclarationMachine.DeclarationControl.<GetSteps>d__d.MoveNext()
   at Microsoft.ActionMachines.Explorer.OpenState.MoveNext()
   at Microsoft.ActionMachines.Explorer.OpenState..ctor(Nullable`1 incomingAction, MachineState state, OpenState previousState, Explorer explorer, Boolean isStart, Int32 pathBound)
   at Microsoft.ActionMachines.Explorer.Explore(IMachine machine)
   at Microsoft.ActionMachines.TransformationMachineProviderBase.Explore(ICompressedState initialState, IMachine machine)
   at Microsoft.ActionMachines.TransformationMachineBase.<GetInitialStates>d__0.MoveNext()
   at Microsoft.ActionMachines.DeclarationMachine.<GetInitialStates>d__0.MoveNext()
   at Microsoft.ActionMachines.Explorer.CreateInitialFrontier(IMachine machine, ICompressedState iniState)
   at Microsoft.ActionMachines.Explorer.Explore(IMachine machine)
   at Microsoft.SpecExplorer.ExploringOperator.Explore()
   at Microsoft.SpecExplorer.RemoteExplorer.Explore(IMachine machine, IConfiguration config)
   at Microsoft.SpecExplorer.RemoteExplorer.Work()
===========
===========
FATAL ERROR: Object reference not set to an instance of an object.
stacktrace:
   at Microsoft.SpecExplorer.VS.SpecExplorerPackage.RecoverFromFatalError(Exception exception)
   at Microsoft.SpecExplorer.RecoverFromFatalErrorEventObserver.HandleEvent(ExplorerEvent e)
   at Microsoft.SpecExplorer.EventManager.HandleEvent(ExplorerEvent e)

involved exception: System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Xrt.State.ActiveState.IsExistential(Term term)
   at Microsoft.Xrt.Background.ConstraintStore.<>c__DisplayClass203.<GetContext>b__1fe(IntPtr t)
   at Microsoft.Xrt.Background.IsVarOrSelectorOnVarOrUnaryOperatorOnVar(IntPtr termPtr, Predicate`1 pred)
   at Microsoft.Xrt.Background.ConstraintStore.GetContext(Predicate`1 isExistential, Boolean removeMetaFunctions)
   at Microsoft.Xrt.Background.SaveNormalizedContext(Predicate`1 isExistential, Boolean removeMetaFunctions)
   at Microsoft.Xrt.State.ActiveState.<>c__DisplayClass2a.<Compress>b__29()
   at Microsoft.Xrt.State.HeapCompressor.Compress(Action collectOther)
   at Microsoft.Xrt.State.ActiveState.CompressHeaps(Action afterObjectHeapConsolidation)
   at Microsoft.Xrt.State.ActiveState.Compress(Boolean doConsolidate, TermSet& freed)
   at Microsoft.Xrt.State.ActiveState.Compress()
   at Microsoft.ActionMachines.RuleMachine.ActivationControlState.CanAssumeActionEquality(Action action, MachineState machineState, Nullable`1 demandedAction, MachineStep& resultStep)
   at Microsoft.ActionMachines.RuleMachine.ActivationControlState.<GetEntryStep>d__59.MoveNext()
   at Microsoft.ActionMachines.RuleMachine.ActivationControlState.<GetSteps>d__2a.MoveNext()
   at Microsoft.ActionMachines.DeclarationMachine.DeclarationControl.<GetSteps>d__d.MoveNext()
   at Microsoft.ActionMachines.ParallelMachine.ParallelControl.<GetCommonSteps>d__33.MoveNext()
   at Microsoft.ActionMachines.ParallelMachine.ParallelControl.<GetSteps>d__12.MoveNext()
   at Microsoft.ActionMachines.DeclarationMachine.DeclarationControl.<GetSteps>d__d.MoveNext()
   at Microsoft.ActionMachines.Explorer.OpenState.MoveNext()
   at Microsoft.ActionMachines.Explorer.OpenState..ctor(Nullable`1 incomingAction, MachineState state, OpenState previousState, Explorer explorer, Boolean isStart, Int32 pathBound)
   at Microsoft.ActionMachines.Explorer.Explore(IMachine machine)
   at Microsoft.ActionMachines.TransformationMachineProviderBase.Explore(ICompressedState initialState, IMachine machine)
   at Microsoft.ActionMachines.TransformationMachineBase.<GetInitialStates>d__0.MoveNext()
   at Microsoft.ActionMachines.DeclarationMachine.<GetInitialStates>d__0.MoveNext()
   at Microsoft.ActionMachines.Explorer.CreateInitialFrontier(IMachine machine, ICompressedState iniState)
   at Microsoft.ActionMachines.Explorer.Explore(IMachine machine)
   at Microsoft.SpecExplorer.ExploringOperator.Explore()
   at Microsoft.SpecExplorer.RemoteExplorer.Explore(IMachine machine, IConfiguration config)
   at Microsoft.SpecExplorer.RemoteExplorer.Work()
===========

Answer 3

Hi Dharma,

a possible cause could be a missing "using System" statement etc. in your cord-file:
http://social.msdn.microsoft.com/Forums/en-US/specexplorer/thread/93a49825-309e-4ea2-89d9-00493c5e7fcc
If this can't solve your error you can send your problematic model here [e-mail].

Answer 4

Hi,

when I replace M{2} by (M;M)  it works, but M{2} does not, where M is my OneInstanceConnectDisconnectScenario. M|||M works, too. 

I am sending my model as an attachment to the speccon address.

Thanks for your help!

Dharma