diff --git a/src/main/java/com/booleworks/logicng/np/SetCover.java b/src/main/java/com/booleworks/logicng/np/SetCover.java index d35d73c8..2af7ded3 100644 --- a/src/main/java/com/booleworks/logicng/np/SetCover.java +++ b/src/main/java/com/booleworks/logicng/np/SetCover.java @@ -67,7 +67,7 @@ public static List> compute(final FormulaFactory f, final Collection< for (final Variable setVar : setMap.keySet()) { solver.addSoftFormula(setVar.negate(f), 1); } - final MaxSATResult maxSATResult = solver.solve().getResult(); + final MaxSATResult maxSATResult = solver.solve(); if (!maxSATResult.isSatisfiable()) { throw new IllegalStateException("Internal optimization problem was not feasible."); } diff --git a/src/main/java/com/booleworks/logicng/solvers/MaxSATSolver.java b/src/main/java/com/booleworks/logicng/solvers/MaxSATSolver.java index 6b718849..1bba35b8 100644 --- a/src/main/java/com/booleworks/logicng/solvers/MaxSATSolver.java +++ b/src/main/java/com/booleworks/logicng/solvers/MaxSATSolver.java @@ -363,8 +363,8 @@ protected void addClause(final Formula formula, final int weight) { * Solves the formula on the solver and returns the result. * @return the result (SAT, UNSAT, Optimum found) */ - public LNGResult solve() { - return solve(NopHandler.get()); + public MaxSATResult solve() { + return solve(NopHandler.get()).getResult(); } /** diff --git a/src/test/java/com/booleworks/logicng/solvers/functions/OptimizationFunctionTest.java b/src/test/java/com/booleworks/logicng/solvers/functions/OptimizationFunctionTest.java index b2a4303b..f2bbf458 100644 --- a/src/test/java/com/booleworks/logicng/solvers/functions/OptimizationFunctionTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/functions/OptimizationFunctionTest.java @@ -418,7 +418,7 @@ private int solveMaxSat(final List formulas, final SortedSet final MaxSATSolver solver) { formulas.forEach(solver::addHardFormula); variables.forEach(v -> solver.addSoftFormula(v.negate(formulas.iterator().next().factory()), 1)); - return solver.solve().getResult().getOptimum(); + return solver.solve().getOptimum(); } private SortedSet satisfiedLiterals(final LNGResult> assignment, @@ -467,8 +467,7 @@ private void testOptimumModel(final Formula formula, final LNGResult solver.addSoftFormula(maximize ? l : l.negate(f), 1)); - final int numSatisfiedOll = satisfiedLiterals( - LNGResult.of(SatResult.sat(solver.solve().getResult().getModel())), literals).size(); + final int numSatisfiedOll = satisfiedLiterals(LNGResult.of(SatResult.sat(solver.solve().getModel())), literals).size(); assertThat(actualNumSatisfied).isEqualTo(numSatisfiedOll); } } else { diff --git a/src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSatLongRunningTest.java b/src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSatLongRunningTest.java index 68045ed3..f128ef5e 100644 --- a/src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSatLongRunningTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/maxsat/MaxSatLongRunningTest.java @@ -9,8 +9,6 @@ import com.booleworks.logicng.LongRunningTag; import com.booleworks.logicng.formulas.FormulaFactory; -import com.booleworks.logicng.handlers.LNGResult; -import com.booleworks.logicng.solvers.MaxSATResult; import com.booleworks.logicng.solvers.MaxSATSolver; import com.booleworks.logicng.solvers.maxsat.algorithms.MaxSATConfig; import org.junit.jupiter.api.Test; @@ -37,16 +35,13 @@ public void testWeightedMaxSat() throws IOException { MaxSATSolver.incWBO(f, MaxSATConfig.builder().weight(MaxSATConfig.WeightStrategy.DIVERSIFY).build()); solvers[2] = MaxSATSolver.incWBO(f); for (final MaxSATSolver solver : solvers) { -// final long start = System.currentTimeMillis(); for (final File file : Objects.requireNonNull(folder.listFiles())) { if (file.getName().endsWith("wcnf")) { solver.reset(); readCnfToSolver(solver, file.getAbsolutePath()); - assertThat(solver.solve().getResult().getOptimum()).isEqualTo(result.get(file.getName())); + assertThat(solver.solve().getOptimum()).isEqualTo(result.get(file.getName())); } } -// final long stop = System.currentTimeMillis(); -// System.out.printf("%-8s: %.2f sec%n", solver.getAlgorithm(), (stop - start) / 1000.0); } } diff --git a/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialMaxSATTest.java b/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialMaxSATTest.java index 9c2caae6..3500b925 100644 --- a/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialMaxSATTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialMaxSATTest.java @@ -80,7 +80,7 @@ public void testWBO() throws IOException { for (int i = 0; i < files.length; i++) { final MaxSATSolver solver = MaxSATSolver.wbo(f, config); readCnfToSolver(solver, "src/test/resources/partialmaxsat/" + files[i]); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(results[i]); } @@ -92,7 +92,7 @@ public void testOLL() throws IOException { for (int i = 0; i < files.length; i++) { final MaxSATSolver solver = MaxSATSolver.oll(f); readCnfToSolver(solver, "src/test/resources/partialmaxsat/" + files[i]); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(results[i]); } @@ -107,7 +107,7 @@ public void testIncWBO() throws IOException { for (int i = 0; i < files.length; i++) { final MaxSATSolver solver = MaxSATSolver.incWBO(f, config); readCnfToSolver(solver, "src/test/resources/partialmaxsat/" + files[i]); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(results[i]); } @@ -129,7 +129,7 @@ public void testLinearSU() throws IOException { for (int i = 0; i < files.length; i++) { final MaxSATSolver solver = MaxSATSolver.linearSU(f, config); readCnfToSolver(solver, "src/test/resources/partialmaxsat/" + files[i]); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(results[i]); } @@ -153,7 +153,7 @@ public void testLinearUS() throws IOException { for (int i = 0; i < files.length; i++) { final MaxSATSolver solver = MaxSATSolver.linearUS(f, config); readCnfToSolver(solver, "src/test/resources/partialmaxsat/" + files[i]); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(results[i]); } @@ -176,7 +176,7 @@ public void testMSU3() throws IOException { for (int i = 0; i < files.length; i++) { final MaxSATSolver solver = MaxSATSolver.msu3(f, config); readCnfToSolver(solver, "src/test/resources/partialmaxsat/" + files[i]); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(results[i]); } @@ -317,7 +317,7 @@ public void testNonClauselSoftConstraints() throws ParserException { for (final MaxSATSolver solver : solvers) { solver.addHardFormula(f.parse("a & b & c")); solver.addSoftFormula(f.parse("~a & ~b & ~c"), 1); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getModel().literals()).containsExactlyInAnyOrder( f.variable("a"), f.variable("b"), f.variable("c") @@ -335,7 +335,7 @@ public void testSoftConstraintsCornerCaseVerum() throws ParserException { solver.addHardFormula(f.parse("a & b & c")); solver.addSoftFormula(f.parse("$true"), 1); solver.addSoftFormula(f.parse("~a & ~b & ~c"), 1); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getModel().literals()).containsExactlyInAnyOrder( f.variable("a"), f.variable("b"), f.variable("c") @@ -353,7 +353,7 @@ public void testSoftConstraintsCornerCaseFalsum() throws ParserException { solver.addHardFormula(f.parse("a & b & c")); solver.addSoftFormula(f.parse("$false"), 1); solver.addSoftFormula(f.parse("~a & ~b & ~c"), 1); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getModel().literals()).containsExactlyInAnyOrder( f.variable("a"), f.variable("b"), f.variable("c") diff --git a/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java b/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java index 329a4e76..b4b3fbbf 100644 --- a/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/maxsat/PartialWeightedMaxSATTest.java @@ -87,7 +87,7 @@ public void testWBO() throws IOException { for (int i = 0; i < files.length; i++) { final MaxSATSolver solver = MaxSATSolver.wbo(f, config); readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/" + files[i]); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(results[i]); } @@ -108,7 +108,7 @@ public void testIncWBO() throws IOException { for (int i = 0; i < files.length; i++) { final MaxSATSolver solver = MaxSATSolver.incWBO(f, config); readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/" + files[i]); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(results[i]); } @@ -127,7 +127,7 @@ public void testLinearSU() throws IOException { for (int i = 0; i < files.length; i++) { final MaxSATSolver solver = MaxSATSolver.linearSU(f, config); readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/" + files[i]); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(results[i]); } @@ -151,7 +151,7 @@ public void testWMSU3() throws IOException { for (int i = 0; i < files.length; i++) { final MaxSATSolver solver = MaxSATSolver.wmsu3(f, config); readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/" + files[i]); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(results[i]); } @@ -168,7 +168,7 @@ public void testWMSU3BMO() throws IOException { for (int i = 0; i < bmoFiles.length; i++) { final MaxSATSolver solver = MaxSATSolver.wmsu3(f, config); readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/bmo/" + bmoFiles[i]); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(bmoResults[i]); } @@ -186,7 +186,7 @@ public void testLineaerSUBMO() throws IOException { for (int i = 0; i < bmoFiles.length; i++) { final MaxSATSolver solver = MaxSATSolver.linearSU(f, config); readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/bmo/" + bmoFiles[i]); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(bmoResults[i]); } @@ -198,14 +198,14 @@ public void testOLL() throws IOException { for (int i = 0; i < bmoFiles.length; i++) { final MaxSATSolver solver = MaxSATSolver.oll(f); readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/bmo/" + bmoFiles[i]); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(bmoResults[i]); } for (int i = 0; i < files.length; i++) { final MaxSATSolver solver = MaxSATSolver.oll(f); readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/" + files[i]); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(results[i]); } @@ -216,7 +216,7 @@ public void testOLL() throws IOException { public void testLargeOLL1() throws IOException { final MaxSATSolver solver = MaxSATSolver.oll(f); readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/large/large_industrial.wcnf"); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(68974); } @@ -226,7 +226,7 @@ public void testLargeOLL1() throws IOException { public void testLargeOLL2() throws IOException { final MaxSATSolver solver = MaxSATSolver.oll(f); readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/large/t3g3-5555.spn.wcnf"); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(1100610); } @@ -236,7 +236,7 @@ public void testLargeOLL2() throws IOException { public void testOLLWithLargeWeights() throws IOException { final MaxSATSolver solver = MaxSATSolver.oll(f); readCnfToSolver(solver, "src/test/resources/partialweightedmaxsat/large/large_weights.wcnf"); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(90912); } @@ -341,7 +341,7 @@ public void testWeightedNonClauseSoftConstraints() throws ParserException { for (final MaxSATSolver solver : solvers) { solver.addHardFormula(f.parse("a & b & c")); solver.addSoftFormula(f.parse("~a & ~b & ~c"), 2); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getModel().literals()).containsExactlyInAnyOrder( f.variable("a"), f.variable("b"), f.variable("c") @@ -362,7 +362,7 @@ public void testWeightedSoftConstraintsCornerCaseVerum() throws ParserException solver.addHardFormula(f.parse("a & b & c")); solver.addSoftFormula(f.parse("$true"), 2); solver.addSoftFormula(f.parse("~a & ~b & ~c"), 3); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getModel().literals()).containsExactlyInAnyOrder( f.variable("a"), f.variable("b"), f.variable("c") @@ -382,7 +382,7 @@ public void testWeightedSoftConstraintsCornerCaseFalsum() throws ParserException solver.addHardFormula(f.parse("a & b & c")); solver.addSoftFormula(f.parse("$false"), 2); solver.addSoftFormula(f.parse("~a & ~b & ~c"), 3); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getModel().literals()).containsExactlyInAnyOrder( f.variable("a"), f.variable("b"), f.variable("c") diff --git a/src/test/java/com/booleworks/logicng/solvers/maxsat/PureMaxSATTest.java b/src/test/java/com/booleworks/logicng/solvers/maxsat/PureMaxSATTest.java index 7b1c7482..a8d9bb0c 100644 --- a/src/test/java/com/booleworks/logicng/solvers/maxsat/PureMaxSATTest.java +++ b/src/test/java/com/booleworks/logicng/solvers/maxsat/PureMaxSATTest.java @@ -98,9 +98,9 @@ public void testCornerCase() throws ParserException { solver.addHardFormula(f.parse("a | b")); solver.addHardFormula(f.verum()); solver.addSoftFormula(A, 1); - MaxSATResult result = solver.solve().getResult(); + MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); - result = solver.solve().getResult(); + result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); } @@ -116,13 +116,13 @@ public void testWBO() throws IOException { for (final String file : files) { final MaxSATSolver solver = MaxSATSolver.wbo(f, config); MaxSATReader.readCnfToSolver(solver, "src/test/resources/maxsat/" + file); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(1); } final MaxSATSolver solver = MaxSATSolver.wbo(f, config); MaxSATReader.readCnfToSolver(solver, "src/test/resources/sat/9symml_gr_rcs_w6.shuffled.cnf"); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(0); } @@ -140,13 +140,13 @@ public void testIncWBO() throws IOException { for (final String file : files) { final MaxSATSolver solver = MaxSATSolver.incWBO(f, config); MaxSATReader.readCnfToSolver(solver, "src/test/resources/maxsat/" + file); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(1); } final MaxSATSolver solver = MaxSATSolver.wbo(f, config); MaxSATReader.readCnfToSolver(solver, "src/test/resources/sat/9symml_gr_rcs_w6.shuffled.cnf"); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(0); } @@ -164,13 +164,13 @@ public void testLinearSU() throws IOException { for (final String file : files) { final MaxSATSolver solver = MaxSATSolver.linearSU(f, config); MaxSATReader.readCnfToSolver(solver, "src/test/resources/maxsat/" + file); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(1); } final MaxSATSolver solver = MaxSATSolver.wbo(f, config); MaxSATReader.readCnfToSolver(solver, "src/test/resources/sat/9symml_gr_rcs_w6.shuffled.cnf"); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(0); } @@ -196,13 +196,13 @@ public void testLinearUS() throws IOException { for (final String file : files) { final MaxSATSolver solver = MaxSATSolver.linearUS(f, config); MaxSATReader.readCnfToSolver(solver, "src/test/resources/maxsat/" + file); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(1); } final MaxSATSolver solver = MaxSATSolver.wbo(f, config); MaxSATReader.readCnfToSolver(solver, "src/test/resources/sat/9symml_gr_rcs_w6.shuffled.cnf"); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(0); } @@ -228,13 +228,13 @@ public void testMSU3() throws IOException { for (final String file : files) { final MaxSATSolver solver = MaxSATSolver.msu3(f, config); MaxSATReader.readCnfToSolver(solver, "src/test/resources/maxsat/" + file); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(1); } final MaxSATSolver solver = MaxSATSolver.wbo(f, config); MaxSATReader.readCnfToSolver(solver, "src/test/resources/sat/9symml_gr_rcs_w6.shuffled.cnf"); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(0); } @@ -246,13 +246,13 @@ public void testOLL() throws IOException { for (final String file : files) { final MaxSATSolver solver = MaxSATSolver.oll(f); MaxSATReader.readCnfToSolver(solver, "src/test/resources/maxsat/" + file); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(1); } final MaxSATSolver solver = MaxSATSolver.oll(f); MaxSATReader.readCnfToSolver(solver, "src/test/resources/sat/9symml_gr_rcs_w6.shuffled.cnf"); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(0); } @@ -262,7 +262,7 @@ public void testSingle() throws IOException { final MaxSATSolver solver = MaxSATSolver.incWBO(f, MaxSATConfig.builder() .cardinality(MaxSATConfig.CardinalityEncoding.MTOTALIZER).verbosity(SOME).output(logStream).build()); readCnfToSolver(solver, "src/test/resources/maxsat/c-fat200-2.clq.cnf"); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(26); final MaxSAT.Stats stats = solver.stats(); @@ -292,7 +292,7 @@ public void testAssignment() throws ParserException { solver.addSoftFormula(p.parse("a"), 1); solver.addSoftFormula(p.parse("~y"), 1); solver.addSoftFormula(p.parse("z"), 1); - final MaxSATResult result = solver.solve().getResult(); + final MaxSATResult result = solver.solve(); assertThat(result.isSatisfiable()).isTrue(); assertThat(result.getOptimum()).isEqualTo(3); final Assignment model = result.getModel();