[Bug] Invalid promela file hello world example.

[bbrockbernd]

Hi. I am quite interested in this project and tried to run gomela on my machine. However, it looks like the created pml files are incorrect. I tried running the hello world example from the README. The pml file it creates is:

// num_comm_params=0
// num_mand_comm_params=0
// num_opt_comm_params=0

// git_link=https://github.com//blob///Users/--/Gomela/source/hello.go#L5
typedef Chandef {
	chan sync = [0] of {bool};
	chan enq = [0] of {bool};
	chan deq = [0] of {bool,bool};
	chan sending = [0] of {bool};
	chan rcving = [0] of {bool};
	chan closing = [0] of {bool};
	int size = 0;
	int num_msgs = 0;
	bool closed = false;
}



init { 
	chan child_main50 = [1] of {int}->
	run main5(child_main50)->
	child_main50?0->
stop_process:skip
}

proctype main5(chan child) {
	bool closed-> 
	bool ok-> 
	int i->
	bool state = true->
	int num_msgs->
	chan child_print171 = [1] of {int}->
	chan child_print170 = [1] of {int}->
	chan ch_ch = [0] of {int}->
	run print17(ch_ch,child_print170)->
	run receiver(child_print170)->
	

	if
	:: ch_ch!0->
	fi->
	run print17(ch_ch,child_print171)->
	run receiver(child_print171)->
	

	if
	:: ch_ch!0->
	fi->
	stop_process: skip->
	child!0
}
proctype print17(Chandef ch_ch;chan child) {
	bool closed-> 
	bool ok-> 
	int i->
	bool state = true->
	int num_msgs->
	

	if /* Send	/Users/--/Gomela/source/hello.go:18:3 */
	:: ch_ch!0->   (<----ERRORS HERE)
	fi->
	stop_process: skip->
	child!0
}

 /* ================================================================================== */
 /* ================================================================================== */
 /* ================================================================================== */ 

SPIN says: "incomplete structure ref 'ch_ch' saw operator: !" Which probably porints to the :: ch_ch!0-> line in the print17 proctype, since ch_ch is a Chandef param and not chan..
I have tried to use multiple go versions: 1.15, 1.16 1.20 and 1.22. (The last one results in SIGSEGV btw..) But no luck...

[VladSaioc]

Hi @bbrockbernd. I see what the issue is, and will try to issue a fix. In the meantime, try to search for the newModel function and set the ContainsClose property to true. Hopefully that will sort out the discrepancy.

Alternatively, try gomela-ase21 for a more stable version of the project.

[bbrockbernd]

Thanks! Are there big differences between this version and the ase21 version? Otherwise ill stick to that one!