Translation Alloy to Electrum: Bad Parenthizing

[esb-dev]

Hi,

Im using Electrum Analyzer 2.1 (forked from Alloy Analyzer 5.1) built 2021-04-21T14:18:04.241Z

The following example shows that the parenthizing seems to be not correct in the generated Electrod code:

open util/graph[Node]
abstract sig Node {
	neighbors: set Node, 
	var parent: lone Node,
	var inbox: set Node 
}

one sig INode extends Node {} -- Initiator
sig PNode extends Node {}     -- Paricipant


fact {
	noSelfLoops[neighbors]     -- irreflexive
	undirected[neighbors]      -- undirected
	rootedAt[neighbors, INode] -- connected with initiator
}

pred skip {
	parent' = parent
	inbox' = inbox
}
	
pred init {
	no parent and no inbox
}

pred broadcast[n, fp: Node] {
	let to = n.neighbors - fp {
		all q: to | q.inbox' = q.inbox + n
		all u: (Node - to) - n | u.inbox' = u.inbox // observe the parenthesis here
		n.inbox' = n.inbox - fp 
	} 
}

pred initiate {
	init
	broadcast[INode, INode]
	parent' = parent
}

pred forward {
	some n: PNode, msg: Node | {
			no n.parent and msg in n.inbox
			parent' = parent ++ n->msg
			broadcast[n, msg] // shouild not send to future parent
	}
}

fact { 
	init
	always {
		initiate or
		forward or
    skip
	}
} 

run { eventually some parent } for exactly 4 Node

/* generated file for Electrod
lines 74 - 77

   (all broadcast_u: (this##INode + this##PNode) - (forward_n . 
    this##Node#neighbors) - forward_msg - forward_n { 
     (broadcast_u . (this##Node#inbox)' ) = (broadcast_u . this##Node#inbox)
     }) and 

corresponding to Node - n.neighbors - msg - n  -- which is not correct

but should be:

   (all broadcast_u: ((this##INode + this##PNode) - (forward_n . 
    this##Node#neighbors - forward_msg)) - forward_n { 
     (broadcast_u . (this##Node#inbox)' ) = (broadcast_u . this##Node#inbox)
     }) and 

corresponding to (Node - (n.neighbors - msg)) - n -- which is correct
*/

Sorry that I don't have a shorter example.

Kind regards,
Burkhardt Renz

[nmacedo]

You're right, it seems parenthesization of the difference operator is lost during translation.

Minimal example:

var sig a {}
var sig b,c in a {}

check { 
	some a - (b - c) iff some a - b - c
}