mtype subtype checking fails when read to fields in typedef

[liuzikai]

For example,

mtype:Symbol = { SYM_A, SYM_B }

typedef St {
  mtype:Symbol sym;
};

chan Channel = [0] of { mtype:Symbol };

proctype Bar() {
  St s;
  Channel ? s.sym;
}

(The code piece is incomplete. It's cherry-picked from a large codebase.)

When running spin on it, it complains:

Error: 's' is type '_unnamed_', but should be type 'Symbol'
Error: incorrect type of 's'

I think spin should check the type of s.sym rather than s? Or do I understand mtype subtyping wrong?

[nimble-code]

thanks for the report.
I'll check it out.

[nimble-code]

I tried to complete your example, to reproduce the problem -- but I do not get the error message you reported:
$ cat subtype.pml
mtype: Symbol = { SYM_A, SYM_B }

typedef St {
mtype:Symbol sym;
};

chan Channel = [0] of { mtype:Symbol };

active proctype Bar() {
St s;
Channel ? s.sym;
}

active proctype Foo() {
mtype:Symbol x = SYM_A;

    Channel ! x

}
$ spin -run subtype.pml

(Spin Version 6.5.2 -- 30 May 2023)
+ Partial Order Reduction

Full statespace search for:
never claim - (none specified)
assertion violations +
cycle checks - (disabled by -DSAFETY)
invalid end states +

State-vector 28 byte, depth reached 4, errors: 0
4 states, stored
0 states, matched
4 transitions (= stored+matched)
0 atomic steps
hash conflicts: 0 (resolved)

Stats on memory usage (in Megabytes):
0.000 equivalent memory usage for states (stored*(State-vector + overhead))
0.292 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage

unreached in proctype Bar
(0 of 2 states)
unreached in proctype Foo
(0 of 2 states)

pan: elapsed time 0 seconds

[liuzikai]

Sorry for the confusion, but it happens in replay rather than output.

With inserting false at one of the proctype, getting a trail, and replaying it, I gets the following:

$ spin -p -replay subtype.pml
  1:    proc  1 (Foo:1) subtype.pml:18 (state 1)        [Channel!x]
spin: subtype.pml:11, Error: 's' is type '_unnamed_', but should be type 'Symbol'
spin: subtype.pml:11, Error: incorrect type of 's'
  2:    proc  0 (Bar:1) subtype.pml:11 (state 1)        [Channel?s.sym]
  3: proc 1 terminates
spin: trail ends after 3 steps
#processes: 1
  3:    proc  0 (Bar:1) subtype.pml:12 (state 2)
2 processes created
$ spin -v                    
Spin Version 6.5.2 -- 6 December 2019
spin: error, no filename specified

Probably it does not affect the correctness. Just that error message is standing out.

[nimble-code]

yes, I can reproduce it now. I made an attempt to fix it, but it gets tricky -- so I'm going to leave it for now.