From 4c5d2900d156ab17edfe23b8d4323ecb59489525 Mon Sep 17 00:00:00 2001 From: Michael Leuschel <leuschel@uni-duesseldorf.de> Date: Mon, 22 Feb 2021 19:18:52 +0100 Subject: [PATCH] add Z version of Button example --- Button/Z/button.json | 30 ++++++++++++++++++++++++++++++ Button/Z/button.tex | 42 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 72 insertions(+) create mode 100644 Button/Z/button.json create mode 100644 Button/Z/button.tex diff --git a/Button/Z/button.json b/Button/Z/button.json new file mode 100644 index 0000000..361c04a --- /dev/null +++ b/Button/Z/button.json @@ -0,0 +1,30 @@ +{ + "svg": "../button.svg", + "items": [ + { + "id": "button", + "attr": "fill", + "value": "IF button=True THEN \"green\" ELSE \"red\" END" + }, + { + "id": "button", + "attr": "stroke-width", + "value": "IF ENABLED(\"pressButton\") THEN 6 ELSE 1 END", + "ignore": "is now used in hover below" + }, + { + "id": "button_%0", + "attr": "visibility", + "value": "\"hidden\"", + "repeat": [ "TRUE", "FALSE" ] + } + ], + "events": [ + { + "id": "button", + "event": "toggleButton", + "hovers": [{ "attr":"stroke-width", "enter":"6", "leave":"1"}, + { "attr":"opacity", "enter":"0.8", "leave":"1.0"}] + } + ] +} diff --git a/Button/Z/button.tex b/Button/Z/button.tex new file mode 100644 index 0000000..d2e1227 --- /dev/null +++ b/Button/Z/button.tex @@ -0,0 +1,42 @@ +\documentclass[a4paper]{article} +\usepackage{fuzz} + +\begin{document} + + +\section*{Button} +\subsection*{Data types} +We define the type for booleans: +\begin{zed} + Bool ::= True | False\\ +\end{zed} + +\subsection*{State} +The current state of the button is a boolean +\begin{schema}{State} + button: Bool +\end{schema} + + +\subsection*{Operations} + +\begin{schema}{pressButton} + \Delta State +\where + button = False\\ + button' = True +\end{schema} + +\begin{schema}{toggleButton} + \Delta State +\where + button' = (\IF button= True \THEN False \ELSE True) +\end{schema} + +\begin{schema}{Init} + State\\ + \where + button = False + \end{schema} + +\end{document} -- GitLab