diff --git a/main.go b/main.go index 127fa95..131645b 100644 --- a/main.go +++ b/main.go @@ -1091,6 +1091,12 @@ func GenerateFailurePath(srcFileName string, failurePath []*modelchecker.Link, i if len(node.Returns) > 0 { fmt.Printf("returns: %s\n", strings.ReplaceAll(node.Returns.String(), lib.SymmetryPrefix, "")) } + if len(node.Roles) > 0 { + for _, role := range node.Roles { + roleStr := strings.ReplaceAll(role.Fields.String(), lib.SymmetryPrefix, "") + fmt.Printf("%s: %s\n", role.RefStringShort(), roleStr) + } + } } fmt.Println("------") if !isPlayground { diff --git a/modelchecker/processor.go b/modelchecker/processor.go index ecc67d1..33a0109 100644 --- a/modelchecker/processor.go +++ b/modelchecker/processor.go @@ -517,6 +517,16 @@ func (n *Node) appendState(p *Process, buf *strings.Builder) { buf.WriteString("Returns: ") buf.WriteString(escapedString) } + if len(p.Roles) > 0 { + for _, role := range p.Roles { + buf.WriteString("\\n") + buf.WriteString(role.RefStringShort()) + buf.WriteString(": ") + fieldsStr := role.Fields.String() + escapedFields := strings.ReplaceAll(fieldsStr, "\"", "\\\"") + buf.WriteString(escapedFields) + } + } } // GetName returns the name