Skip to content
Snippets Groups Projects
Commit 213edbd2 authored by Fabian Vu's avatar Fabian Vu
Browse files

Add more information on machines

parent f1718240
No related branches found
No related tags found
No related merge requests found
Pipeline #146412 passed
Showing
with 74 additions and 5 deletions
/*
From ProB Examples
*/
MACHINE Generated100 MACHINE Generated100
CONSTANTS CONSTANTS
c100, c100,
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE INTEGERSET_Laws MACHINE INTEGERSET_Laws
INVARIANT INVARIANT
(0..4 = 1..4 \/ {0}) & (0..4 = 1..4 \/ {0}) &
......
/*
From ProB Examples
*/
MACHINE IncrementalStatePackingTestLargeSlow MACHINE IncrementalStatePackingTestLargeSlow
SETS SETS
ID={aa,bb,cc} ID={aa,bb,cc}
......
/*
From ProB Examples
*/
MACHINE IncrementalStatePackingTestLargeSlow2 MACHINE IncrementalStatePackingTestLargeSlow2
SETS SETS
ID={aa,bb,cc} ID={aa,bb,cc}
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE NatRangeLaws MACHINE NatRangeLaws
VARIABLES xx,zz VARIABLES xx,zz
INVARIANT INVARIANT
......
/*
Original model from Event-B:
L. Ladenberger, D. Hansen, H. Wiegard, J. Bendisposto, and M. Leuschel. Validation of the ABZ landing gear system using ProB. In Int. J. Softw. Tools Technol. Transf., 19(2):187–203, Apr. 2017.
Translated to Classical B manually
*/
MACHINE Ref5_Switch MACHINE Ref5_Switch
SETS /* enumerated */ SETS /* enumerated */
DOOR_STATE={open,closed,door_moving}; DOOR_STATE={open,closed,door_moving};
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE RelLaws_BOOL1 MACHINE RelLaws_BOOL1
// BOOL is BOOL // BOOL is BOOL
/* This machine is intended so that you can check whether ProB deals /* This machine is intended so that you can check whether ProB deals
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE SeqLaws MACHINE SeqLaws
SETS SETS
setY = {y1,y2} setY = {y1,y2}
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE SetLaws MACHINE SetLaws
SETS /* enumerated */ SETS /* enumerated */
setX={el1,el2,el3} setX={el1,el2,el3}
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE SetLawsNat MACHINE SetLawsNat
VARIABLES VARIABLES
SS, TT, VV SS, TT, VV
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE SetLawsNatural MACHINE SetLawsNatural
VARIABLES VARIABLES
SS, TT, VV SS, TT, VV
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE SetLawsPow MACHINE SetLawsPow
SETS /* enumerated */ SETS /* enumerated */
elements={el1} elements={el1}
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE SetLawsPow2 MACHINE SetLawsPow2
SETS /* enumerated */ SETS /* enumerated */
elements={el1,el2} elements={el1,el2}
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE SetLawsPowPow MACHINE SetLawsPowPow
SETS /* enumerated */ SETS /* enumerated */
elements={el1} elements={el1}
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE SetLawsPowPowCart MACHINE SetLawsPowPowCart
SETS /* enumerated */ SETS /* enumerated */
elements={el1} elements={el1}
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE SetRelLaws_NatBool MACHINE SetRelLaws_NatBool
/* SETS /* SETS
......
/*
From ProB Examples, originally used to test ProB
*/
MACHINE SetRelationConstructs MACHINE SetRelationConstructs
VARIABLES basea, a, baseb, b, basec, c VARIABLES basea, a, baseb, b, basec, c
INVARIANT INVARIANT
......
/*
Written by Michael Leuschel
*/
MACHINE Sieve MACHINE Sieve
VARIABLES numbers,cur, limit VARIABLES numbers,cur, limit
INVARIANT INVARIANT
......
/*
Written by Michael Leuschel
*/
MACHINE SieveParallel MACHINE SieveParallel
VARIABLES numbers,cur, limit VARIABLES numbers,cur, limit
INVARIANT INVARIANT
......
/*
Model of Simpson's four slot algorithm
*/
MACHINE Simpson_Four_Slot MACHINE Simpson_Four_Slot
SETS SETS
INDEX = {p0,p1,s0,s1}; INDEX = {p0,p1,s0,s1};
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment