001 /* This file is part of the project "Hilbert II" - http://www.qedeq.org
002 *
003 * Copyright 2000-2011, Michael Meyling <mime@qedeq.org>.
004 *
005 * "Hilbert II" is free software; you can redistribute
006 * it and/or modify it under the terms of the GNU General Public
007 * License as published by the Free Software Foundation; either
008 * version 2 of the License, or (at your option) any later version.
009 *
010 * This program is distributed in the hope that it will be useful,
011 * but WITHOUT ANY WARRANTY; without even the implied warranty of
012 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
013 * GNU General Public License for more details.
014 */
015
016 package org.qedeq.kernel.bo.logic.model;
017
018
019 /**
020 * A model for our mathematical world. It has entities, functions and predicates.
021 * There are also predicate and function constants.
022 *
023 * @author Michael Meyling
024 */
025 public final class SixDynamicModel extends DynamicModel {
026
027 /** "Zero" or empty set. */
028 public static final Entity EMPTY = new Entity(0, "{}", "{} or empty set");
029
030 /** "One" or set that contains the empty set. */
031 public static final Entity ZERO_ONE = new Entity(1, "1", "1");
032
033 /** "Two" or set that contains "zero" and "one". */
034 public static final Entity ZERO_TWO = new Entity(2, "2", "2");
035
036 /** "One" or set that contains the empty set. */
037 public static final Entity ONE_ONE = new Entity(3, "{1}", "{1}");
038
039 /** "Two" or set that contains "zero" and "one". */
040 public static final Entity ONE_TWO = new Entity(4, "{2}", "{2}");
041
042 /** "Two" or set that contains "zero" and "one". */
043 public static final Entity TWO_ONE_TWO = new Entity(5, "{1, 2}", "{1, 2}");
044
045 /** Map to empty class. */
046 public static final Function FUNCTION_EMPTY = Function.createConstant(EMPTY);
047
048 /** Map to 1. */
049 public static final Function FUNCTION_ZERO_ONE = Function.createConstant(ZERO_ONE);
050
051 /** Map to 2. */
052 public static final Function FUNCTION_ZERO_TWO = Function.createConstant(ZERO_TWO);
053
054 /** Map to {1}. */
055 public static final Function FUNCTION_ONE_ONE = Function.createConstant(ONE_ONE);
056
057 /** Map to {2}. */
058 public static final Function FUNCTION_ONE_TWO = Function.createConstant(ONE_TWO);
059
060 /** Map to {1, 2}. */
061 public static final Function FUNCTION_TWO_ONE_TWO = Function.createConstant(TWO_ONE_TWO);
062
063 /** Return true if all values are zero. */
064 public static final Predicate IS_EMPTY = Predicate.isEntity(EMPTY);
065
066 /** Return true if all values are 1. */
067 public static final Predicate IS_ZERO_ONE = Predicate.isEntity(ZERO_ONE);
068
069 /** Return true if all values are 2. */
070 public static final Predicate IS_ZERO_TWO = Predicate.isEntity(ZERO_TWO);
071
072 /** Return true if all values are {1}. */
073 public static final Predicate IS_ONE_ONE = Predicate.isEntity(ONE_ONE);
074
075 /** Return true if all values are {2}. */
076 public static final Predicate IS_ONE_TWO = Predicate.isEntity(ONE_TWO);
077
078 /** Return true if all values are {2}. */
079 public static final Predicate IS_TWO_ONE_TWO = Predicate.isEntity(TWO_ONE_TWO);
080
081 /** Are the entities are not all equal to {2}? */
082 public static final Predicate NOT_IS_ONE_TWO = Predicate.not(IS_ONE_TWO);
083
084 /** Map to one. */
085 /** Modulo 3. */
086 private final Function functionModulo3 = new Function(0, 99, "% 3", "modulo 3") {
087 public Entity map(final Entity[] entities) {
088 int result = 0;
089 for (int i = 0; i < entities.length; i++) {
090 result += entities[i].getValue() % 3;
091 }
092 result = result % 3;
093 return getEntity(result);
094 }
095 };
096
097 /** +1 Modulo 3. */
098 private final Function functionPlus1Modulo3 = new Function(0, 99, "+1 % 3", "plus 1 modulo 3") {
099 public Entity map(final Entity[] entities) {
100 int result = 1;
101 for (int i = 0; i < entities.length; i++) {
102 result += entities[i].getValue() % 3;
103 }
104 result = result % 3;
105 return getEntity(result);
106 }
107 };
108
109
110 /**
111 * Constructor.
112 */
113 public SixDynamicModel() {
114 super("six elements");
115
116 addEntity(EMPTY);
117 addEntity(ZERO_ONE);
118 addEntity(ZERO_TWO);
119 addEntity(ONE_ONE);
120 addEntity(ONE_TWO);
121 addEntity(TWO_ONE_TWO);
122
123 addFunction(0, FUNCTION_EMPTY);
124 addFunction(0, FUNCTION_ZERO_ONE);
125 addFunction(0, FUNCTION_ZERO_TWO);
126 addFunction(0, FUNCTION_ONE_ONE);
127 addFunction(0, FUNCTION_ONE_TWO);
128 addFunction(0, FUNCTION_TWO_ONE_TWO);
129
130 addFunction(1, FUNCTION_EMPTY);
131 addFunction(1, FUNCTION_ZERO_ONE);
132 addFunction(1, functionModulo3);
133 addFunction(1, functionPlus1Modulo3);
134
135 addFunction(2, FUNCTION_EMPTY);
136 addFunction(2, FUNCTION_ZERO_ONE);
137 addFunction(2, functionModulo3);
138 addFunction(2, functionPlus1Modulo3);
139
140 addPredicate(0, FALSE);
141 addPredicate(0, TRUE);
142
143 addPredicate(1, FALSE);
144 addPredicate(1, TRUE);
145 addPredicate(1, EVEN);
146 addPredicate(1, IS_EMPTY);
147 addPredicate(1, IS_ZERO_ONE);
148 addPredicate(1, IS_ZERO_TWO);
149 addPredicate(1, IS_ONE_ONE);
150 addPredicate(1, IS_TWO_ONE_TWO);
151
152 addPredicate(2, FALSE);
153 addPredicate(2, TRUE);
154 addPredicate(2, EVEN);
155 addPredicate(2, LESS);
156 addPredicate(2, EQUAL);
157 addPredicate(2, IS_EMPTY);
158 addPredicate(2, IS_ZERO_ONE);
159 addPredicate(2, IS_ZERO_TWO);
160 addPredicate(2, IS_ONE_ONE);
161 addPredicate(2, IS_ONE_TWO);
162
163 addPredicateConstant(new ModelPredicateConstant("in", 2), new Predicate(2, 2, "in", "isSet") {
164 public boolean calculate(final Entity[] entities) {
165 boolean result = false;
166 final int a = entities[0].getValue();
167 final int b = entities[1].getValue();
168 if (a == 1 && (b == 3 || b == 5)) {
169 result = true;
170 }
171 if (a == 2 && (b == 4 || b == 5)) {
172 result = true;
173 }
174 return result;
175 }
176 });
177 }
178
179 public String getDescription() {
180 return "This model has six entities: {}, {1}, {2}, {{1}}, {{2}} and {1, 2}.";
181 }
182
183 public Entity comprehension(final Entity[] array) {
184 Entity result = EMPTY;
185 for (int i = 0; i < array.length; i++) {
186 switch (array[i].getValue()) {
187 case 0:
188 case 3:
189 case 4:
190 case 5: break;
191 case 1: if (result.getValue() != 5) {
192 if (result.getValue() == 0) {
193 result = ONE_ONE;
194 } else if (result.getValue() == 4) {
195 result = TWO_ONE_TWO;
196 }
197 }
198 break;
199 case 2: if (result.getValue() != 5) {
200 if (result.getValue() == 0) {
201 result = ONE_TWO;
202 } else if (result.getValue() == 4) {
203 result = TWO_ONE_TWO;
204 }
205 }
206 break;
207 default: throw new RuntimeException("unknown value for entity " + array[i]);
208 }
209 }
210 return result;
211 }
212
213 }
|