Skip to content

Instantly share code, notes, and snippets.

@hwayne
Last active May 11, 2020
Embed
What would you like to do?
Formal Methods Example Spec
EXTENDS Integers, TLC, Sequences
CONSTANTS Devices
(* --algorithm BatchInstall
variables
AppScope \in [Devices -> {0, 1}];
Installs \in [Devices -> BOOLEAN];
batch_pool = {};
lock = FALSE;
define
PoolNotEmpty == batch_pool # {}
end define
procedure ChangeAppScope()
variables cache;
begin
GetLock:
await ~lock;
lock := TRUE;
Cache:
cache := batch_pool;
Filter:
cache := cache \intersect {d \in Devices: AppScope[d] = 0};
Add:
AppScope := [d \in Devices |->
IF d \in cache THEN AppScope[d] + 1
ELSE AppScope[d]
];
Clean:
batch_pool := batch_pool \ cache;
lock := FALSE;
return;
end procedure
fair process SyncDevice \in Devices
begin
Sync:
if Installs[self] then
batch_pool := batch_pool \union {self};
end if;
if PoolNotEmpty then
either
call ChangeAppScope();
or
skip;
end either;
end if;
end process;
fair process TimeLoop = 0
begin
Start:
while TRUE do
await PoolNotEmpty;
call ChangeAppScope();
end while;
end process
end algorithm;
EXTENDS Integers, TLC, Sequences
CONSTANTS Devices
(* --algorithm BatchInstall
variables
AppScope \in [Devices -> {0, 1}];
Installs \in [Devices -> BOOLEAN];
batch_pool = {};
define
PoolNotEmpty == batch_pool # {}
end define
procedure ChangeAppScope()
begin
Add:
AppScope := [d \in Devices |->
IF d \in batch_pool THEN AppScope[d] + 1
ELSE AppScope[d]
];
Clean:
batch_pool := {};
return;
end procedure
fair process SyncDevice \in Devices
begin
Sync:
if Installs[self] then
batch_pool := batch_pool \union {self};
end if;
end process;
fair process TimeLoop = 0
begin
Start:
while TRUE do
await PoolNotEmpty;
call ChangeAppScope();
end while;
end process
end algorithm; *)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment