- Main Page
- Namespaces
- Classes
- Files
- Related Pages

# /Users/fpy/titan-1-5-MBARI/Mers/Solvers/SAT/GATSAT/unit-tests/TestUniformUnsat1.cpp

    00001
    00002 //
    00003 // Copyright (c) 2004           Model-based Embedded and Robotic Systems Group
    00004 // All Rights Reserved          Massachusetts Institute of Technology
    00005 //
    00006 // This software is provided as is. Model-based Embedded and Robotic Systems
    00007 // (MERS) group does not assume any responsibility.
    00008 //
    00010
    00011 #include "GatsatTester.h"
    00012
    00013 #include <tut.h>
    00014
    00015 using Mers::Models::Base::BaseModelVariable;
    00016
    00017 namespace Mers {
    00018         namespace Solvers {
    00019                 namespace SAT {
    00020                         namespace GATSAT {
    00021                                 namespace unit_tests {
    00022                                         // This should be a macro defined in the including class
    00023                                         namespace c_TestNamespace {
    00024
    00029                                                 class UniformUnsat1Data : public GatsatTester
    00030                                                 {
    00031                                                 public:
    00035                                                         UniformUnsat1Data() : GatsatTester()
    00036                                                         {
    00037                                                                 // The order in which we are defining our domains.
    00038                                                                 enum Domain {
    00039                                                                         OnOffCommand = 0, OnOffValues = 1, SwitchMode = 2,
    00040                                                                         TransChoice = 3
    00041                                                                 };
    00042
    00043                                                                 // The values of our domains.
    00044                                                                 const char * d1Vals[] = {"On", "Off", "No-Command", NULL};
    00045                                                                 const char * d2Vals[] = {"On", "Off", NULL};
    00046                                                                 const char * d3Vals[] = {"Broken", "Off", "On", NULL};
    00047                                                                 const char * d4Vals[] = {"toBroken", "toOff", "toOn", NULL};
    00048
    00049                                                                 // Our domains
    00050                                                                 const struct BMDomainEntry domains[] = {
    00051                                                                         {"On-Off-Command", d1Vals},
    00052                                                                         {"On-Off-Values", d2Vals},
    00053                                                                         {"Switch-Mode", d3Vals},
    00054                                                                         {"Transition-Choice", d4Vals}
    00055                                                                 };
    00056                                                                 unsigned int numDoms = sizeof(domains) / sizeof(domains[0]);
    00057
    00058                                                                 // All of our variables.
    00059                                                                 const struct BMVariableEntry variables[] = {
    00060                                                                         // Search Variable, Variable Name, Domain Index,
    00061                                                                         // Variable Type
    00062                                                                         // 0
    00063                                                                         {"Switch2.mode", SwitchMode,
    00064                                                                          BaseModelVariable::State},
    00065                                                                         // 1
    00066                                                                         {"Switch2.IndicatorLamp", OnOffValues,
    00067                                                                          BaseModelVariable::Observable},
    00068                                                                         // 2
    00069                                                                         {"Switch2.CommandIn", OnOffCommand,
    00070                                                                          BaseModelVariable::Control},
    00071                                                                         // 3
    00072                                                                         {"Switch1.mode", SwitchMode,
    00073                                                                          BaseModelVariable::State},
    00074                                                                         // 4
    00075                                                                         {"Switch1.IndicatorLamp", OnOffValues,
    00076                                                                          BaseModelVariable::Observable},
    00077                                                                         // 5
    00078                                                                         {"Switch1.CommandIn", OnOffCommand,
    00079                                                                          BaseModelVariable::Control},
    00080                                                                         // 6
    00081                                                                         {"Switch2.mode'", SwitchMode,
    00082                                                                          BaseModelVariable::State},
    00083                                                                         // 7
    00084                                                                         {"Switch1.mode'", SwitchMode,
    00085                                                                          BaseModelVariable::State},
    00086                                                                         // 8
    00087                                                                         {"Switch2.trans", TransChoice,
    00088                                                                          BaseModelVariable::Control},
    00089                                                                         // 9
    00090                                                                         {"Switch1.trans", TransChoice,
    00091                                                                          BaseModelVariable::Control}
    00092                                                                 };
    00093                                                                 const unsigned int numVars =
    00094                                                                         sizeof(variables) / sizeof(variables[0]);
    00095
    00096                                                                 // The search variables - in this case the state variables.
    00097                                                                 const unsigned int searchVars[] = {
    00098                                                                         0, 3
    00099                                                                 };
    00100                                                                 unsigned int numSearchVars =
    00101                                                                         sizeof(searchVars) / sizeof(searchVars[0]);
    00102
    00103                                                                 // Our theory
    00104                                                                 const int clauseData[][numVars] = {
    00105                                                                         // !(Switch2 = On) v (Switch2.Lamp = On)
    00106                                                                         {-3, 1, 0, 0, 0, 0, 0, 0, 0, 0},
    00107                                                                         // !(Switch2 = Off) v (Switch2.Lamp = Off)
    00108                                                                         {-2, 2, 0, 0, 0, 0, 0, 0, 0, 0},
    00109                                                                         // !(Switch1 = On) v (Switch1.Lamp = On)
    00110                                                                         {0, 0, 0, -3, 1, 0, 0, 0, 0, 0},
    00111                                                                         // !(Switch1 = Off) v (Switch1.Lamp = Off)
    00112                                                                         {0, 0, 0, -2, 2, 0, 0, 0, 0, 0},
    00113                                                                         // !(Switch2' = On) v !(Switch2.Command = Off) v
    00114                                                                         // !(Switch2.trans = toOff) v (Switch2 = Off)
    00115                                                                         {2, 0, -2, 0, 0, 0, -3, 0, -2, 0},
    00116                                                                         // !(Switch2' = Off) v !(Switch2.Command = On) v
    00117                                                                         // !(Switch2.trans = toOn) v (Switch2 = On)
    00118                                                                         {3, 0, -1, 0, 0, 0, -2, 0, -3, 0},
    00119                                                                         // !(Switch1' = On) v !(Switch1.Command = Off) v
    00120                                                                         // !(Switch1.trans = toOff) v (Switch1 = Off)
    00121                                                                         {0, 0, 0, 2, 0, -2, 0, -3, 0, -2},
    00122                                                                         // !(Switch1' = Off) v !(Switch1.Command = On) v
    00123                                                                         // !(Switch1.trans = toOn) v (Switch1 = On)
    00124                                                                         {0, 0, 0, 3, 0, -1, 0, -2, 0, -3},
    00125                                                                         // !(Switch2' = Off) v !(Switch2.trans = toBroken) v
    00126                                                                         // (Switch2 = Broken)
    00127                                                                         {1, 0, 0, 0, 0, 0, -2, 0, -1, 0},
    00128                                                                         // !(Switch2' = On) v !(Switch2.trans = toBroken) v
    00129                                                                         // (Switch2 = Broken)
    00130                                                                         {1, 0, 0, 0, 0, 0, -3, 0, -1, 0},
    00131                                                                         // !(Switch2' = Broken) v !(Switch2.trans = toBroken) v
    00132                                                                         // (Switch2 = Broken)
    00133                                                                         {1, 0, 0, 0, 0, 0, -1, 0, -1, 0},
    00134                                                                         // !(Switch2' = On) v !(Switch2.trans = toOn) v
    00135                                                                         // (Switch2 = On)
    00136                                                                         {3, 0, 0, 0, 0, 0, -3, 0, -3, 0},
    00137                                                                         // !(Switch2' = Off) v !(Switch2.trans = toOff) v
    00138                                                                         // (Switch2 = Off)
    00139                                                                         {2, 0, 0, 0, 0, 0, -2, 0, -2, 0},
    00140                                                                         // !(Switch1' = Off) v !(Switch1.trans = toBroken) v
    00141                                                                         // (Switch1 = Broken)
    00142                                                                         {0, 0, 0, 1, 0, 0, 0, -2, 0, -1},
    00143                                                                         // !(Switch1' = On) v !(Switch1.trans = toBroken) v
    00144                                                                         // (Switch1 = Broken)
    00145                                                                         {0, 0, 0, 1, 0, 0, 0, -3, 0, -1},
    00146                                                                         // !(Switch1' = Broken) v !(Switch1.trans = toBroken) v
    00147                                                                         // (Switch1 = Broken)
    00148                                                                         {0, 0, 0, 1, 0, 0, 0, -1, 0, -1},
    00149                                                                         // !(Switch1' = On) v !(Switch1.trans = toOn) v
    00150                                                                         // (Switch1 = On)
    00151                                                                         {0, 0, 0, 3, 0, 0, 0, -3, 0, -3},
    00152                                                                         // !(Switch1' = Off) v !(Switch1.trans = toOff) v
    00153                                                                         // (Switch1 = Off)
    00154                                                                         {0, 0, 0, 2, 0, 0, 0, -2, 0, -2}
    00155                                                                 };
    00156
    00157                                                                 unsigned int numClauses =
    00158                                                                         sizeof(clauseData) / sizeof(clauseData[0]);
    00159
    00160                                                                 // This is defined by the file that includes us.
    00161                                                                 t_GatsatUniformFactoryType factory;
    00162
    00163                                                                 initGATSAT(numDoms, domains, numVars, variables,
    00164                                                                         numSearchVars, searchVars, numClauses, clauseData,
    00165                                                                         factory);
    00166                                                         }
    00167
    00171                                                         virtual ~UniformUnsat1Data() {
    00172                                                         }
    00173                                                 };
    00174
    00175                                         }
    00176                                 }
    00177                         }
    00178                 }
    00179         }
    00180 }
    00181
    00182 using Mers::Solvers::SAT::GATSAT::unit_tests::c_TestNamespace::UniformUnsat1Data;
    00183
    00184 namespace{
    00185         typedef tut::test_group<UniformUnsat1Data> t_UniformUnsat1Factory;
    00186         typedef t_UniformUnsat1Factory::object t_UniformUnsat1Object;
    00187
    00189         t_UniformUnsat1Factory uniformUnsat1Factory(c_GatsatName
    00190                 " test of a uniform cost unsatisfaction problem #1");
    00191 }
    00192
    00193 namespace tut {
    00197         template<> template<>
    00198         void t_UniformUnsat1Object::test<1>()
    00199         {
    00200                 // The index of no value
    00201                 //unsigned int noVal = (unsigned int) -1;
    00202
    00203                 // Our expected answer (none)
    00204                 const unsigned int expectedResultsData[][2] = {
    00205                 };
    00206                 unsigned int numResults =
    00207                         sizeof(expectedResultsData) / sizeof(expectedResultsData[0]);
    00208
    00209                 // Our initial constraint (none)
    00210                 const int initialClauseData[][2] = {// Var 0, Var 1
    00211                 };
    00212                 const unsigned int numClauses =
    00213                         sizeof(initialClauseData) / sizeof(initialClauseData[0]);
    00214
    00215                 // Test our test case.
    00216                 testGATSAT(numClauses, initialClauseData,
    00217                                    numResults, expectedResultsData, false, true);
    00218         }
    00219
    00225         template<> template<>
    00226         void t_UniformUnsat1Object::test<2>()
    00227         {
    00228                 // The index of no value
    00229                 //unsigned int noVal = (unsigned int) -1;
    00230
    00231                 // Our expected answer (Sw1=On, Sw2=Off)
    00232                 const unsigned int expectedResultsData[][2] = {
    00233                         {1, 2}
    00234                 };
    00235                 unsigned int numResults =
    00236                         sizeof(expectedResultsData) / sizeof(expectedResultsData[0]);
    00237
    00238                 // Our initial constraint !(Sw1=On) v !(Sw2=Off)
    00239                 const int initialClauseData[][10] = {
    00240                         // !(Switch2 = Off) v !(Switch1 = On)
    00241                         {-2, 0, 0, -3, 0, 0, 0, 0, 0, 0}
    00242                 };
    00243                 const unsigned int numClauses =
    00244                         sizeof(initialClauseData) / sizeof(initialClauseData[0]);
    00245
    00246                 // Test our test case.
    00247                 testGATSAT(numClauses, initialClauseData,
    00248                                    numResults, expectedResultsData, false, true);
    00249         }
    00250
    00256         template<> template<>
    00257         void t_UniformUnsat1Object::test<3>()
    00258         {
    00259                 // The index of no value
    00260                 //unsigned int noVal = (unsigned int) -1;
    00261
    00262                 // Our expected answer (Sw1=On, Sw2=Off)
    00263                 const unsigned int expectedResultsData[][2] = {
    00264                         {2, 2}
    00265                 };
    00266                 unsigned int numResults =
    00267                         sizeof(expectedResultsData) / sizeof(expectedResultsData[0]);
    00268
    00269                 // Our initial constraint !(Sw1.Lamp=On) v !(Sw2.Lamp=On)
    00270                 const int initialClauseData[][10] = {
    00271                         // !(Switch2.Lamp = On) v !(Switch1.Lamp = On)
    00272                         {0, -1, 0, 0, -1, 0, 0, 0, 0, 0}
    00273                 };
    00274                 const unsigned int numClauses =
    00275                         sizeof(initialClauseData) / sizeof(initialClauseData[0]);
    00276
    00277                 // Test our test case.
    00278                 testGATSAT(numClauses, initialClauseData,
    00279                                    numResults, expectedResultsData, false, true);
    00280         }
    00281 }
    00282
    00283