[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!