Issues while implementing Dijkstra's Token Ring Algorithm in Verse

[dassarthak18]

The following error was observed when we were trying to run an implementation of Dijkstra's token ring algorithm in Verse:

Traceback (most recent call last): File "/Users/sarthak/Verse-library/demo/dijkstra/token_ring_distributed.py", line 44, in myagent0 = TokenRingAgent('agent0', file_name=mutualExclusionAlgorithm) File "/Users/sarthak/Verse-library/demo/dijkstra/dijkstra_agent.py", line 15, in init super().init(id, code, file_name) File "/Users/sarthak/Verse-library/verse/agents/base_agent.py", line 27, in init self.decision_logic: ControllerIR = ControllerIR.parse(code, file_name) File "/Users/sarthak/Verse-library/verse/parser/parser.py", line 267, in parse return ControllerIR.from_env(Env.parse(code, fn)) File "/Users/sarthak/Verse-library/verse/parser/parser.py", line 361, in parse proc(root, env) File "/Users/sarthak/Verse-library/verse/parser/parser.py", line 613, in proc if proc(node, env) == START_OF_MAIN: File "/Users/sarthak/Verse-library/verse/parser/parser.py", line 655, in proc env.set(node.name, Lambda.from_ast(node, env)) File "/Users/sarthak/Verse-library/verse/parser/parser.py", line 199, in from_ast ret = proc(node, env) File "/Users/sarthak/Verse-library/verse/parser/parser.py", line 638, in proc proc_assign(node.targets[0], node.value, env) File "/Users/sarthak/Verse-library/verse/parser/parser.py", line 580, in proc_assign val = proc(val, env) File "/Users/sarthak/Verse-library/verse/parser/parser.py", line 728, in proc fun = proc(node.func, env) File "/Users/sarthak/Verse-library/verse/parser/parser.py", line 653, in proc return obj[node.attr] TypeError: 'NoneType' object is not subscriptable

Please find attached model files here.

[crides]

Given this controller (pasted here for convenience)

def controller(ego: State, others: List[State]):
    '''implements the token ring algorithm'''
    output = copy.deepcopy(ego)

    if any( (ego.pid == 0 and other.pid == 2 and ego.x == other.x) for other in others): # Process 0 has token
        output.x = (ego.x + 1) % k
    if any (ego.pid != 0 and (ego.pid == other.pid + 1) and (ego.x != other.x) for other in others):
        # this process is not process 0 and it has the token
        output.x = other.x
    return output

Neither copy and other are bound/in scope. Though, I don't think we support % (modulus) in verify, and this kind of "choose one from a list with arbitrary condition" functionality yet.

I will add proper error messages for this kind of error.