Issue with "------State 0-------" line in getRawInstances output

[AthenaSchulz]

The getRawInstances and getRawInstancesWith function from the Language.Alloy.Debug module seems to produce ByteStrings with a "------State 0-------" line under certain circumstances, which does not seem to be handled well by the parseInstance function (or functions like getInstances that use those internally).

Sample output of getRawInstances with that issue:

 loop=0
end=0
integers={-32, -31, -30, -29, -28, -27, -26, -25, -24, -23, -22, -21, -20, -19, -18, -17, -16, -15, -14, -13, -12, -11, -10, -9, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31}
------State 0-------
univ={ObjectNodes$0, ObjectNodes$1, ObjectNodes$2, ObjectNodes$3, MergeNodes$0, MergeNodes$1, JoinNodes$0, InitialNodes$0, ForkNodes$0, DecisionNodes$0, DecisionNodes$1, ActivityFinalNodes$0, ActivityEdges$0, ActivityEdges$1, ActivityEdges$2, ActivityEdges$3, ActivityEdges$4, ActivityEdges$5, ActivityEdges$6, ActivityEdges$7, ActivityEdges$8, ActivityEdges$9, ActivityEdges$10, ActivityEdges$11, ActivityEdges$12, ActivityEdges$13, ActivityEdges$14, GuardNames$0, GuardNames$1, ComponentNames$0, ComponentNames$1, ComponentNames$2, ComponentNames$3, PlantUMLRepeatBlocks$0, PlantUMLIfElseBlocks$0, PlantUMLForkBlocks$0, PlantUMLSequenceBlocks$0, PlantUMLSequenceBlocks$1, PlantUMLSequenceBlocks$2, PlantUMLSequenceBlocks$3, PlantUMLSequenceBlocks$4, -32, -31, -30, -29, -28, -27, -26, -25, -24, -23, -22, -21, -20, -19, -18, -17, -16, -15, -14, -13, -12, -11, -10, -9, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31}
Int={-32, -31, -30, -29, -28, -27, -26, -25, -24, -23, -22, -21, -20, -19, -18, -17, -16, -15, -14, -13, -12, -11, -10, -9, -8, -7, -6, -5, -4, -3, -2, -1, 0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31}
seq/Int={0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14}
String={}
none={}
this/InitialNodes={InitialNodes$0}
this/FlowFinalNodes={}
this/ActivityFinalNodes={ActivityFinalNodes$0}
this/FinalNodes={ActivityFinalNodes$0}
this/ForkNodes={ForkNodes$0}
this/JoinNodes={JoinNodes$0}
this/MergeNodes={MergeNodes$0, MergeNodes$1}
this/DecisionNodes={DecisionNodes$0, DecisionNodes$1}
this/ControlNodes={MergeNodes$0, MergeNodes$1, JoinNodes$0, InitialNodes$0, ForkNodes$0, DecisionNodes$0, DecisionNodes$1, ActivityFinalNodes$0}
this/ActionNodes={}
this/ObjectNodes={ObjectNodes$0, ObjectNodes$1, ObjectNodes$2, ObjectNodes$3}
this/ActionObjectNodes={ObjectNodes$0, ObjectNodes$1, ObjectNodes$2, ObjectNodes$3}
this/ActionObjectNodes<:name={ObjectNodes$0->ComponentNames$3, ObjectNodes$1->ComponentNames$2, ObjectNodes$2->ComponentNames$1, ObjectNodes$3->ComponentNames$0}
this/ActivityNodes={ObjectNodes$0, ObjectNodes$1, ObjectNodes$2, ObjectNodes$3, MergeNodes$0, MergeNodes$1, JoinNodes$0, InitialNodes$0, ForkNodes$0, DecisionNodes$0, DecisionNodes$1, ActivityFinalNodes$0}
this/ActivityEdges={ActivityEdges$0, ActivityEdges$1, ActivityEdges$2, ActivityEdges$3, ActivityEdges$4, ActivityEdges$5, ActivityEdges$6, ActivityEdges$7, ActivityEdges$8, ActivityEdges$9, ActivityEdges$10, ActivityEdges$11, ActivityEdges$12, ActivityEdges$13, ActivityEdges$14}
this/ActivityEdges<:from={ActivityEdges$0->DecisionNodes$1, ActivityEdges$1->DecisionNodes$1, ActivityEdges$2->DecisionNodes$0, ActivityEdges$3->DecisionNodes$0, ActivityEdges$4->ForkNodes$0, ActivityEdges$5->ForkNodes$0, ActivityEdges$6->ForkNodes$0, ActivityEdges$7->InitialNodes$0, ActivityEdges$8->JoinNodes$0, ActivityEdges$9->MergeNodes$1, ActivityEdges$10->MergeNodes$0, ActivityEdges$11->ObjectNodes$3, ActivityEdges$12->ObjectNodes$2, ActivityEdges$13->ObjectNodes$1, ActivityEdges$14->ObjectNodes$0}
this/ActivityEdges<:to={ActivityEdges$0->ObjectNodes$1, ActivityEdges$1->ObjectNodes$3, ActivityEdges$2->MergeNodes$0, ActivityEdges$3->ActivityFinalNodes$0, ActivityEdges$4->DecisionNodes$1, ActivityEdges$5->ObjectNodes$0, ActivityEdges$6->ObjectNodes$2, ActivityEdges$7->MergeNodes$0, ActivityEdges$8->DecisionNodes$0, ActivityEdges$9->JoinNodes$0, ActivityEdges$10->ForkNodes$0, ActivityEdges$11->MergeNodes$1, ActivityEdges$12->JoinNodes$0, ActivityEdges$13->MergeNodes$1, ActivityEdges$14->JoinNodes$0}
this/ActivityEdges<:guard={ActivityEdges$0->GuardNames$1, ActivityEdges$1->GuardNames$0, ActivityEdges$2->GuardNames$1, ActivityEdges$3->GuardNames$0}
this/GuardNames={GuardNames$0, GuardNames$1}
this/ComponentNames={ComponentNames$0, ComponentNames$1, ComponentNames$2, ComponentNames$3}
this/PlantUMLSequenceBlocks={PlantUMLSequenceBlocks$0, PlantUMLSequenceBlocks$1, PlantUMLSequenceBlocks$2, PlantUMLSequenceBlocks$3, PlantUMLSequenceBlocks$4}
this/PlantUMLRepeatBlocks={PlantUMLRepeatBlocks$0}
this/PlantUMLRepeatBlocks<:repeatStart={PlantUMLRepeatBlocks$0->MergeNodes$0}
this/PlantUMLRepeatBlocks<:body={PlantUMLRepeatBlocks$0->PlantUMLForkBlocks$0}
this/PlantUMLRepeatBlocks<:repeatEnd={PlantUMLRepeatBlocks$0->DecisionNodes$0}
this/PlantUMLIfElseBlocks={PlantUMLIfElseBlocks$0}
this/PlantUMLIfElseBlocks<:ifElseStart={PlantUMLIfElseBlocks$0->DecisionNodes$1}
this/PlantUMLIfElseBlocks<:ifBody={PlantUMLIfElseBlocks$0->PlantUMLSequenceBlocks$3}
this/PlantUMLIfElseBlocks<:elseBody={PlantUMLIfElseBlocks$0->PlantUMLSequenceBlocks$1}
this/PlantUMLIfElseBlocks<:ifElseEnd={PlantUMLIfElseBlocks$0->MergeNodes$1}
this/PlantUMLForkBlocks={PlantUMLForkBlocks$0}
this/PlantUMLForkBlocks<:forkStart={PlantUMLForkBlocks$0->ForkNodes$0}
this/PlantUMLForkBlocks<:bodies={PlantUMLForkBlocks$0->PlantUMLIfElseBlocks$0, PlantUMLForkBlocks$0->PlantUMLSequenceBlocks$2, PlantUMLForkBlocks$0->PlantUMLSequenceBlocks$4}
this/PlantUMLForkBlocks<:forkEnd={PlantUMLForkBlocks$0->JoinNodes$0}
this/PlantUMLBlocks={PlantUMLRepeatBlocks$0, PlantUMLIfElseBlocks$0, PlantUMLForkBlocks$0, PlantUMLSequenceBlocks$0, PlantUMLSequenceBlocks$1, PlantUMLSequenceBlocks$2, PlantUMLSequenceBlocks$3, PlantUMLSequenceBlocks$4}
this/PlantUMLBlocks<:nodes={PlantUMLRepeatBlocks$0->MergeNodes$0, PlantUMLRepeatBlocks$0->DecisionNodes$0, PlantUMLIfElseBlocks$0->MergeNodes$1, PlantUMLIfElseBlocks$0->DecisionNodes$1, PlantUMLForkBlocks$0->JoinNodes$0, PlantUMLForkBlocks$0->ForkNodes$0, PlantUMLSequenceBlocks$0->ActivityFinalNodes$0, PlantUMLSequenceBlocks$1->ObjectNodes$3, PlantUMLSequenceBlocks$2->ObjectNodes$2, PlantUMLSequenceBlocks$3->ObjectNodes$1, PlantUMLSequenceBlocks$4->ObjectNodes$0}
this/PlantUMLBlocks<:substructures={PlantUMLRepeatBlocks$0->PlantUMLForkBlocks$0, PlantUMLIfElseBlocks$0->PlantUMLSequenceBlocks$1, PlantUMLIfElseBlocks$0->PlantUMLSequenceBlocks$3, PlantUMLForkBlocks$0->PlantUMLIfElseBlocks$0, PlantUMLForkBlocks$0->PlantUMLSequenceBlocks$2, PlantUMLForkBlocks$0->PlantUMLSequenceBlocks$4}
skolem $generate_ie1={PlantUMLIfElseBlocks$0}
skolem $generate_fb1={PlantUMLForkBlocks$0}

with which only loop, end and integers seem to be recognized by parseInstance.

For more information see also: https://github.com/fmidue/ba-athena-schulz/issues/7

[marcellussiegburg]

I guess this happened by using features of Alloy 6.0.0 (mutable state)? Could you provide the original Alloy code leading to this error (i.e. the actual parameters of getInstances)?

[AthenaSchulz]

getInstances was originally called on https://github.com/fmidue/ba-athena-schulz/blob/master/src/AD_Alloy.hs#L38 in that module, to which the corresponding alloy files concatenated in there can be found here: https://github.com/fmidue/ba-athena-schulz/tree/master/alloy/ad

Node that this problem also appeared when just using https://github.com/fmidue/ba-athena-schulz/blob/master/alloy/ad/ad_components_sig.als (with a predicate and a run-statement attached at the end)

If you dont have access to that repo, I could send you the files you are interested in privately