From 91bd2bfaa5f95ff988ff36af64f153b608e0c63c Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Wed, 22 Nov 2023 20:43:14 +0100
Subject: [PATCH] add Sieve example
Signed-off-by: Michael Leuschel <leuschel@uni-duesseldorf.de>
---
Sieve/Sieve_VisB.mch | 46 ++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 46 insertions(+)
create mode 100644 Sieve/Sieve_VisB.mch
diff --git a/Sieve/Sieve_VisB.mch b/Sieve/Sieve_VisB.mch
new file mode 100644
index 0000000..30f001a
--- /dev/null
+++ b/Sieve/Sieve_VisB.mch
@@ -0,0 +1,46 @@
+MACHINE Sieve_VisB
+// A version of the Sieve model with a simple VisB visualisation
+DEFINITIONS
+ SET_PREF_MAXINT == 99;
+ SET_PREF_MININT == -1;
+ MINLIM == MAXINT-1;
+ GOAL == (cur=1 & numbers /= {});
+ VISB_SVG_FILE == "";
+ VISB_SVG_BOX == rec(height:220, width:220, viewBox:"0 0 220 220");
+ vsz == 20;
+ VISB_SVG_OBJECTS2 == {x,y•x:0..9 & y:0..9 | rec(`id`:("nr",x,y), svg_class:"text",
+ x:vsz+x*vsz, y:vsz+y*vsz, `font-size`:10,
+ text:x+y*10)};
+ VISB_SVG_OBJECTS1 == {x,y•x:0..9 & y:0..9 | rec(`id`:("rec",x,y), svg_class:"rect",
+ x:15+x*vsz, y:5+y*vsz,
+ stroke:"green", `stroke-width`:1.5,fill:"white",
+ width:vsz-1, height:vsz-1)};
+ VISB_SVG_UPDATES2 == {x,y•x:0..9 & y:0..9 | rec(`id`:("rec",x,y),
+ stroke:IF x+y*10=cur THEN "red"
+ ELSIF x+y*10:numbers THEN "green" ELSE "gray" END,
+ fill: IF x+y*10:numbers THEN "white" ELSE "gray" END)};
+VARIABLES numbers,cur, limit
+INVARIANT
+ numbers <: INTEGER & cur:NATURAL1 & limit:NATURAL1
+INITIALISATION numbers := {} || cur := 1 || limit := 1
+OPERATIONS
+ StartSieve(lim) = PRE cur=1 & lim>MINLIM & lim <= MAXINT THEN
+ numbers := 2..lim ||
+ cur := 2 ||
+ limit := lim
+ END;
+ prime <-- TreatNumber(cc) = PRE cc=cur & cur>1 & cur*cur<= limit THEN
+ IF cc:numbers THEN
+ numbers := numbers - ran(%n.(n:cur..limit/cur|cur*n))
+/* numbers := numbers - ran(%n.(n:2..limit/cur|cur*n)) */
+ || prime := TRUE
+ ELSE
+ prime := FALSE
+ END ||
+ cur := cur+1
+ END;
+ r <-- Finish = PRE cur*cur>limit THEN
+ cur := 1 || r := card(numbers)
+ END
+END
+
--
GitLab