From 6b69e329cbd6413543b28162df361d8518c9bdfa Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Fri, 4 Dec 2015 07:52:09 +0100
Subject: [PATCH] fixed typo
---
src/main/java/de/tlc4b/TLC4B.java | 5 +-
.../resources/standardModules/Functions.tla | 56 +++++++++----------
2 files changed, 31 insertions(+), 30 deletions(-)
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 747e300..667c8a5 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -41,8 +41,9 @@ public class TLC4B {
private String constantsSetup;
public static void main(String[] args) {
- System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up
- // windows
+ System.setProperty("apple.awt.UIElement", "true");
+ // avoiding pop up window
+
TLC4B tlc4b = new TLC4B();
try {
tlc4b.process(args);
diff --git a/src/main/resources/standardModules/Functions.tla b/src/main/resources/standardModules/Functions.tla
index 21da3ea..7e9d2bb 100644
--- a/src/main/resources/standardModules/Functions.tla
+++ b/src/main/resources/standardModules/Functions.tla
@@ -3,38 +3,38 @@ EXTENDS FiniteSets
Range(f) == {f[x] : x \in DOMAIN f}
\* The range of the function f
-
+
Image(f,S) == {f[x] : x \in S \cap DOMAIN f}
\* The image of the set S for the function f
-
-Card(f) == Cardinality(DOMAIN f)
+
+Card(f) == Cardinality(DOMAIN f)
\* The Cardinality of the function f
Id(S) == [x \in S|-> x]
\* The identity function on set S
-DomRes(S, f) == [x \in (S \cap DOMAIN f) |-> f[x]]
+DomRes(S, f) == [x \in (S \cap DOMAIN f) |-> f[x]]
\* The restriction on the domain of f for set S
-DomSub(S, f) == [x \in DOMAIN f \ S |-> f[x]]
+DomSub(S, f) == [x \in DOMAIN f \ S |-> f[x]]
\* The subtraction on the domain of f for set S
-RanRes(f, S) == [x \in {y \in DOMAIN f: f[y] \in S} |-> f[x]]
+RanRes(f, S) == [x \in {y \in DOMAIN f: f[y] \in S} |-> f[x]]
\* The restriction on the range of f for set S
-
-RanSub(f, S) == [x \in {y \in DOMAIN f: f[y] \notin S} |-> f[x]]
+
+RanSub(f, S) == [x \in {y \in DOMAIN f: f[y] \notin S} |-> f[x]]
\* The subtraction on the range of f for set S
-
+
Inverse(f) == {<<f[x],x>>: x \in DOMAIN f}
- \* The inverser relation of the function f
+ \* The inverse relation of the function f
-Override(f, g) == [x \in (DOMAIN f) \cup DOMAIN g |-> IF x \in DOMAIN g THEN g[x] ELSE f[x]]
+Override(f, g) == [x \in (DOMAIN f) \cup DOMAIN g |-> IF x \in DOMAIN g THEN g[x] ELSE f[x]]
\* Overwriting of the function f with the function g
-
-FuncAssign(f, d, e) == Override(f, [x \in {d} |-> e])
+
+FuncAssign(f, d, e) == [f EXCEPT ![d] = e]
\* Overwriting the function f at index d with value e
-
-TotalInjFunc(S, T) == {f \in [S -> T]:
+
+TotalInjFunc(S, T) == {f \in [S -> T]:
Cardinality(DOMAIN f) = Cardinality(Range(f))}
\* The set of all total injective functions
@@ -44,22 +44,22 @@ TotalSurFunc(S, T) == {f \in [S -> T]: T = Range(f)}
TotalBijFunc(S, T) == {f \in [S -> T]: T = Range(f) /\
Cardinality(DOMAIN f) = Cardinality(Range(f))}
\* The set of all total bijective functions
-
+
ParFunc(S, T) == UNION{[x -> T] :x \in SUBSET S}
\* The set of all partial functions
ParFuncEleOf(f, S, T) == {x \in {f} : DOMAIN f \subseteq S /\ Range(f) \subseteq T}
\* The set containing f if f is a partial function
-
-isEleOfParFunc(f, S, T) == DOMAIN f \subseteq S /\ Range(f) \subseteq T
+
+isEleOfParFunc(f, S, T) == DOMAIN f \subseteq S /\ Range(f) \subseteq T
\* Test if the function f is a partial function
-
+
ParInjFunc(S, T)== {f \in ParFunc(S, T):
Cardinality(DOMAIN f) = Cardinality(Range(f))}
\* The set of all partial injective functions
-ParInjFuncEleOf(f, S, T)== {x \in {f}:
- /\ DOMAIN f \subseteq S
+ParInjFuncEleOf(f, S, T)== {x \in {f}:
+ /\ DOMAIN f \subseteq S
/\ Range(f) \subseteq T
/\ Cardinality(DOMAIN f) = Cardinality(Range(f))}
\* The set containing f if f is a partial injective function
@@ -67,21 +67,21 @@ ParInjFuncEleOf(f, S, T)== {x \in {f}:
ParSurFunc(S, T)== {f \in ParFunc(S, T): T = Range(f)}
\* The set of all partial surjective function
-ParSurFuncEleOf(f, S, T)== {x \in {f}:
- /\ DOMAIN f \subseteq S
+ParSurFuncEleOf(f, S, T)== {x \in {f}:
+ /\ DOMAIN f \subseteq S
/\ Range(f) \subseteq T
/\ T = Range(f)}
\* The set containing f if f is a partial surjective function
-ParBijFunc(S, T) == {f \in ParFunc(S, T):
+ParBijFunc(S, T) == {f \in ParFunc(S, T):
/\ Range(f) = T
/\ Cardinality(DOMAIN f) = Cardinality(Range(f))}
\* The set of all partial bijective functions
-
-ParBijFuncEleOf(f, S, T) == {x \in {f}:
- /\ DOMAIN f \subseteq S
+
+ParBijFuncEleOf(f, S, T) == {x \in {f}:
+ /\ DOMAIN f \subseteq S
/\ Range(f) \subseteq T
/\ Cardinality(DOMAIN f) = Cardinality(Range(f))
/\ T = Range(f)}
-\* The set containing f if f is a partial bijective function
+\* The set containing f if f is a partial bijective function
=============================================================================
--
GitLab