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

Add information to machines

parent a9bb2c81
Branches
No related tags found
No related merge requests found
Pipeline #146410 passed
Showing
with 88 additions and 22 deletions
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE ArithmeticExpLaws MACHINE ArithmeticExpLaws
// some specific laws about exponentiation // some specific laws about exponentiation
// kept separate from other laws because of CLP(FD) overflow issues // kept separate from other laws because of CLP(FD) overflow issues
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE ArithmeticLaws MACHINE ArithmeticLaws
ABSTRACT_VARIABLES ABSTRACT_VARIABLES
x, x,
......
/*
From ProB Examples
*/
MACHINE Bakery0 MACHINE Bakery0
VARIABLES aa VARIABLES aa
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE BoolLaws MACHINE BoolLaws
CONSTANTS CONSTANTS
TT,FF TT,FF
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE BoolLaws_SetCompr MACHINE BoolLaws_SetCompr
/* Boolean Laws expressed using set comprehensions */ /* Boolean Laws expressed using set comprehensions */
CONSTANTS CONSTANTS
......
/*
From ProB Examples, originally used to test ProB
*/
MACHINE BoolWithArithLaws MACHINE BoolWithArithLaws
/* ada(x>2)ed version of BoolLaws, to check b_interpreter_check, which /* ada(x>2)ed version of BoolLaws, to check b_interpreter_check, which
has a special (1<=1)eatment for arithmetic operators */ has a special (1<=1)eatment for arithmetic operators */
......
/*
Developed by J.Colley
*/
MACHINE CAN_BUS_tlc MACHINE CAN_BUS_tlc
SETS SETS
......
MACHINE EqualityLaws // rewritten from prob_examples for b2program /*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE EqualityLaws
SETS SETS
ID={i1,i2,i3} ID={i1,i2,i3}
VARIABLES a,b,c, s1, d,e VARIABLES a,b,c, s1, d,e
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE ExplicitChecks MACHINE ExplicitChecks
VARIABLES VARIABLES
x x
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE ExplicitChecks_Old MACHINE ExplicitChecks_Old
VARIABLES VARIABLES
x x
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE ExplicitComputations MACHINE ExplicitComputations
/* A machine with some explicitly given results for certain computations */ /* A machine with some explicitly given results for certain computations */
SETS SETS
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE ExplicitComputations2 MACHINE ExplicitComputations2
/* A machine with some explicitly given results for certain computations */ /* A machine with some explicitly given results for certain computations */
SETS SETS
......
/*
From ProB Examples, originally used to test ProB,
rewritten for B2Program
*/
MACHINE FunLaws MACHINE FunLaws
/* This machine is intended so that you can check whether ProB deals /* This machine is intended so that you can check whether ProB deals
with basic laws associated to functions and relations. ProB should with basic laws associated to functions and relations. ProB should
......
/*
From ProB Examples
*/
MACHINE GCD MACHINE GCD
VARIABLES x,y VARIABLES x,y
INVARIANT INVARIANT
......
/*
Developed by Fabian Vu for Open AI Environment
*/
MACHINE HighwayEnvironment MACHINE HighwayEnvironment
SETS SETS
......
/*
Developed by Fabian Vu for Open AI Environment
*/
MACHINE HighwayEnvironment2 MACHINE HighwayEnvironment2
SETS SETS
......
/*
Developed by Fabian Vu for OpenAI Environment
*/
MACHINE LunarLander MACHINE LunarLander
VARIABLES x, y, v_x, v_y, angle, v_angular, left_leg_on_ground, right_leg_on_ground VARIABLES x, y, v_x, v_y, angle, v_angular, left_leg_on_ground, right_leg_on_ground
......
/*
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 LandingGear_R6 MACHINE LandingGear_R6
SETS /* enumerated */ SETS /* enumerated */
DOOR_STATE={open,closed,door_moving}; DOOR_STATE={open,closed,door_moving};
......
<?xml-stylesheet href="landinggear.css" type="text/css"?> <?xml-stylesheet href="landinggear.css" type="text/css"?>
<!-- From 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. !-->
<svg width="947" height="728" xmlns="http://www.w3.org/2000/svg" id="landinggear" xmlns:xlink="http://www.w3.org/1999/xlink"> <svg width="947" height="728" xmlns="http://www.w3.org/2000/svg" id="landinggear" xmlns:xlink="http://www.w3.org/1999/xlink">
<metadata id="metadata3467">image/svg+xml</metadata> <metadata id="metadata3467">image/svg+xml</metadata>
......
<!-- From 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. !-->
<svg width="947" height="728" xmlns="http://www.w3.org/2000/svg" id="landinggear" xmlns:xlink="http://www.w3.org/1999/xlink"> <svg width="947" height="728" xmlns="http://www.w3.org/2000/svg" id="landinggear" xmlns:xlink="http://www.w3.org/1999/xlink">
<metadata id="metadata3467">image/svg+xml</metadata> <metadata id="metadata3467">image/svg+xml</metadata>
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment