[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Sean McCauliff <sean.mc...@xxxxxxxxx>*Date*: Sat, 2 Feb 2019 19:30:36 -0800 (PST)

Is this a known issue? Should I ask about this on github instead?

Hitting CRTL-T does nothing. I don't see anything in .metadata/.log

This is the entire spec.

Thanks,

Sean

-------------------------------- MODULE wire --------------------------------

EXTENDS Integers

(*-- algorithm wire

variables

people = {"alice", "bob"},

acc = [p \in people |-> 5],

sender = "alice",

receiver = "bob",

amount = 3;

define

NoOverdrafts == \A p \in people: acc[p] >= 0

end define;

begin

Withdraw:

acc[sender] := acc[sender] - amount;

Deposit:

acc[receiver] := acc[receiver] + amount;

end algorithm; *)

=============================================================================

EXTENDS Integers

(*-- algorithm wire

variables

people = {"alice", "bob"},

acc = [p \in people |-> 5],

sender = "alice",

receiver = "bob",

amount = 3;

define

NoOverdrafts == \A p \in people: acc[p] >= 0

end define;

begin

Withdraw:

acc[sender] := acc[sender] - amount;

Deposit:

acc[receiver] := acc[receiver] + amount;

end algorithm; *)

=============================================================================

**Follow-Ups**:**Re: Plus Cal Translation Does Nothing***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] What if every action could use all the variables? Would we need to define Init?** - Next by Date:
**Re: Plus Cal Translation Does Nothing** - Previous by thread:
**Re: Please help with temporal formula** - Next by thread:
**Re: Plus Cal Translation Does Nothing** - Index(es):