Cell bag detection

Reproduce the report with the provided strange.k definition using the kompile command, then read the cell-bag diagnostic and its source location. Check the blocked issue 3167 and related feature discussion in issue 1419; done should mean the requested behavior or guidance is clear for this configuration.

Blocked on: https://github.com/runtimeverification/k/issues/3167

What component is the issue in?

Front-End

Which command

• kompile
• kast
• krun
• kprove
• kprovex
• ksearch

What K Version?

K version: v5.5.38

Operating System

Linux

K Definitions (If Possible)

module STRANGE
  imports DOMAINS

  configuration
    <top>
      <nextid> 1 </nextid>          //Last generated fresh int value
      <ch> .Map </ch>               //Map of channel names to types
      <nset> .Map </nset>           //Map of named sets to actual sets
      <procstrs>                    //Bag to store process structures
        <procstr multiplicity="*">
          <pmodel> .K </pmodel>     //The name given in the proc. definition
          <pact> .Map </pact>       //Map of action names to definitions
          <psch> .Map </psch>       //Map of schema names to definitions
          <pdef> .K </pdef>         //The whole process definition text
          <pstate> .Map </pstate>   //A map from state var names to types
          <pinv> .K </pinv>         //The state constraint
        </procstr>
      </procstrs>
      <deadlock> .Set </deadlock>   //Set with ids of deadlocked processes
      <tempset> .Set </tempset>     //Used for converting circus set to K sets
      <procs>                       //Configuration for each running action
        <proc color="green" multiplicity="*">
          <model> .K </model>       //The declared name for the process
          <k>$PGM:K</k>             //The K Cell -- The computation cell
          <id>0</id>                //An unique integer reference
          <alt>0</alt>              //Id to the alternative of an ext. choice
          <parent>0</parent>        //Reference to the proc. which spawned
          <env> .Map </env>         //A map from var names to symbolic values
          <postenv> .Map </postenv> //Like env but used in schemas decor. vars.
          <stack> .List </stack>    //Stack of environments for nested scopes
          <sync>false</sync>        //Flag a process waiting an initial exec.
          <const>true</const>       //The constraint as in the OPS
          <temp> .K </temp>         //Auxiliary K manipulation
        </proc>
      </procs>
      <inits>                       //Set of initials waiting for resolution
        <init multiplicity="*">
          <iresp> 0 </iresp>        //The current responsible for the initial
          <iev> .K </iev>           //The communication event
          <from> .Set </from>       //References to all concerning processes
          <ialt> .Set </ialt>       //Reference to alternatives for ext. choice
          <iexp> .K </iexp>
        </init>
      </inits>
      <oks>                         //Set of notifications of solved initials
        <ok multiplicity="*">
          <oev> .K </oev>           //The resolved communication event
          <to> .Set </to>           //References to the concerning processes
        </ok>
      </oks>
      <spectr> .K </spectr>         //The specification trace
      <tr> .K </tr>                 //The observable output CS trace
    </top>

endmodule

Steps to Reproduce

kompile strange.k

Expected Results

[Error] Compiler: Cell bags are only supported on the Java backend. If you want
this feature, comment on https://github.com/runtimeverification/k/issues/1419 .
As a workaround, you can add the attribute type="Set" and add a unique
identifier to each element in the set.
	Source(~/strange/strange.k)
	Location(5,5,53,11)
	   .	    v~~~~
	 5 |	    <top>
	   |		...
	53 |	    </top>
	   .	    ~~~~~^
[Error] Compiler: Had 1 structural errors.

I don't understand what cell bags are, and where I need to put `type="Set".