Hi,
I am trying to model a system in which an element can be inserted into any possible location in a container,and I am using an instance-based solution Modeling.
I would like to create a scenario that insert an element after the head element. I am using the following script to simulate the scenario, but it does not work, and spec explorer crashes.The root reason seems to be "object for instance field selection
neither reference nor compound nor native".
machine RandomInsertWithOneItem(DlinkAdapter container) : Main where ForExploration = true
{
(let DLinkedListNode<string> newNode
in
((. newNode!= container.GetHead() .):container.InsertAfter("c",newNode)))
}
Here is the Debug Log:
FATAL ERROR: Executor failure:
Xrt Stacktrace:
at DlinkTest.DlinkAdapter.GetHead
at CordCode.constraint_5(DlinkTest.DlinkAdapter,DataStructures.DLinkedListNode<System.String>)
stacktrace:
在 Microsoft.SpecExplorer.VS.SpecExplorerPackage.RecoverFromFatalError(Exception exception)
在 Microsoft.SpecExplorer.RecoverFromFatalErrorEventObserver.HandleEvent(ExplorerEvent e)
在 Microsoft.SpecExplorer.EventManager.HandleEvent(ExplorerEvent e)
involved exception: Microsoft.Xrt.Execution.ExecutionFatalErrorException: Executor failure:
Xrt Stacktrace:
at DlinkTest.DlinkAdapter.GetHead
at CordCode.constraint_5(DlinkTest.DlinkAdapter,DataStructures.DLinkedListNode<System.String>)
---> Microsoft.Xrt.RecoverFromFatalErrorException: object for instance field selection neither reference nor compound nor native
I have two questions here.
1. how to get a reference to a single element from a container?
2. what is wrong with the the method "getHead"?
Thanks in advance.