wneuper/isac: src/java-tests/isac/bridge/TestBridge.java@c6e6c271ee07

     1 /*

     2  * #############################################################################

     3  * ATTENTION: BridgeMain must be started because of BridgeRMI (design fault) !?!

     4  * #############################################################################

     5  *

     6  * @author Walther Neuper, member of the ISAC-team, Copyright (c) 2004 by

     7  * Walther Neuper created Aug 30, 2004, 11:58:35 AM Institute for

     8  * Softwaretechnology, Graz University of Technology, Austria.

     9  *

    10  * Use is subject to license terms.

    11  */

    12 package isac.bridge;

    14 import java.io.File;

    15 import java.io.FileInputStream;

    16 import java.io.FileOutputStream;

    17 import java.io.IOException;

    18 import java.io.ObjectInputStream;

    19 import java.io.ObjectOutputStream;

    20 import java.util.Vector;

    22 import org.apache.log4j.Logger;

    24 import isac.interfaces.ICalcElement;

    25 import isac.interfaces.ICalcIterator;

    26 import isac.interfaces.IToCalc;

    27 import isac.interfaces.IToUser;

    28 import isac.kestore.KEStoreServices;

    29 import isac.util.CalcChanged;

    30 import isac.util.Formalization;

    31 import isac.util.formulae.Assumptions;

    32 import isac.util.formulae.CalcHead;

    33 import isac.util.formulae.CalcFormula;

    34 import isac.util.formulae.Formula;

    35 import isac.util.formulae.Position;

    36 import isac.util.parser.FormalizationDigest;

    37 import isac.util.tactics.Tactic;

    38 import junit.framework.TestCase;

    40 /**

    41  * @author Walther Neuper Aug 30, 2004, 11:58:35 AM

    42  *

    43  * ATTENTION: if these tests fail,

    44  * @see {isac.util.parser.TestFormalizationDigest.java} if formalization has

    45  *      changed, i.e. if there is an error to be handled first:

    46  *

    47  * the file 'step_a.fmz' is _VERY_ sensible against changes in Formalization, it

    48  * is copied from isac/util/parser/data/exp_IsacCore_Tests_1b.fmz

    49  */

    50 public class TestBridge extends TestCase {

    52     static Logger logger_ = Logger.getLogger(MathEngine.class.getName());

    54     /**

    55      * tests the example 'IsacCore/Tests/minipbl_with_mini-subpbl' comprising UC

    56      * 'start auto calculation' \label{SPECIFY:START:auto}

    57      *

    58      */

    59     public void testMinisubpblAutoCalc() throws Exception {

    60         System.out

    61                 .println("---BEGIN isac.bridge.TestBridge#testMinisubpblAutoCalc");

    63         //load the file of the example,

    64         //see TestKEStoreServices#testLoadContentMinisubpbl

    65         KEStoreServices ks = new KEStoreServices("isac/xmldata");

    66         Vector vec = ks.loadContent("exp", "exp_IsacCore_Tests_1b.xml");

    67         //parse out the Formalization

    68         //see TestFormalizationDigest#testParseExplMini

    69         String xmlstr = (String) vec.firstElement();

    70         FormalizationDigest fd = new FormalizationDigest();

    71         Formalization fmz = fd.parseFormalization((String) xmlstr);

    72         System.out.println(".end step_a-----");

    74         //start the calculation

    75         MathEngine.init("localhost");

    76         MathEngine me = MathEngine.getMathEngine();

    78         IToCalc ct = me.getCalcTree(fmz);

    79         IToUser user = new MockIToUser();

    80         ct.addDataChangeListener(user);

    81         CalcChanged cce = null;

    82         System.out.println(".end step_a-----");

    83         //end step_a

    84         // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

    86         ct.completeCalcHead();

    87         // sent to bridge: autoCalculate 1 CompleteCalcHead;

    88         ICalcIterator ci = ct.getActiveFormula();

    89         //######^ drop: push addDataChangeListener towards/into

    90         //######^ startCalculation and fetch ci from CalcChanged:

    91         //ci = (ICalcIterator) cce.getLastGeneratedFormula().clone();

    92         CalcHead ch = (CalcHead) ci.getFormula();

    93         System.out.println(".end step_b-----");

    94         //end step_b

    95         // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

    97         //autoCalculate

    98         System.out.println(".autoCalculate");

    99         ct.autoCalculate(IToCalc.SCOPE_CALCULATION, 0);

   101         cce = ((MockIToUser) user).getCalcChangedEvent();

   102         assertEquals("unchanged", cce.getLastUnchangedFormula().toSMLString(),

   103                 "([],Met)");

   104         assertEquals("deleted", cce.getLastDeletedFormula().toSMLString(),

   105                 "([],Met)");

   106         assertEquals("generated", cce.getLastGeneratedFormula().toSMLString(),

   107                 "([],Res)");

   108         System.out.println(".end step_c-----");

   109         //end step_c

   110         // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   112         //display the steps generated

   113         Object fch = null;

   114         ci = (ICalcIterator) cce.getLastUnchangedFormula().cloneIterator();

   115         int i = 0;

   116         // while (ci.compareTo(cce.getLastGeneratedFormula()) < 0) {

   117         // i++;

   118         // boolean b = ci.moveDown();

   119         // System.out.print("..iterator at " + ci.toSMLString());

   120         // fch = ci.getFormula();

   121         // System.out.println(" yields "

   122         // + ((ICalcElement) fch).toSMLString());

   123         // }

   124         Vector elems = cce.getLastUnchangedFormula().getFormulaeFromTo(

   125                 cce.getLastGeneratedFormula(), new Integer(2), false);

   126         for (i = 0; i < elems.size(); i++) {

   127             System.out.println(" yields "

   128                     + ((ICalcElement) elems.elementAt(i)).toSMLString());

   129         }

   130         System.out.println("mini-auto: steps= " + i);

   131         assertEquals("mini-auto: steps= ", i, 10);

   132         assertEquals("mini-auto: last step", ((ICalcElement) elems

   133                 .elementAt(i - 1)).toSMLString(), "[x = 1]");

   134         System.out.println(".end step_d-----");

   135         //end step_d

   136         // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   138         logger_.debug("---END isac.bridge.TestBridge#testMinisubpblAutoCalc");

   139         System.out

   140                 .println("---END isac.bridge.TestBridge#testMinisubpblAutoCalc");

   141     }

   143     /***************************************************************************

   144      * tests the example 'IsacCore/Tests/minipbl_with_mini-subpbl' comprising UC

   145      * 'start interactive calculation' \label{SPECIFY:START:interactive} +

   146      * \label{SOLVE:AUTO:one}}

   147      *

   148      * step_a like above

   149      */

   150     public void testMinisubpblNextStep() throws Exception {

   151         System.out

   152                 .println("---BEGIN isac.bridge.TestBridge#testMinisubpblNextStep");

   154         //load the file of the example,

   155         //see TestKEStoreServices#testLoadContentMinisubpbl

   156         KEStoreServices ks = new KEStoreServices("isac/xmldata");

   157         Vector vec = ks.loadContent("exp", "exp_IsacCore_Tests_1b.xml");

   158         //parse out the Formalization

   159         //see TestFormalizationDigest#testParseExplMini

   160         String xmlstr = (String) vec.firstElement();

   161         FormalizationDigest fd = new FormalizationDigest();

   162         Formalization fmz = fd.parseFormalization((String) xmlstr);

   163         System.out.println(".end step_a-----");

   165         //start the calculation

   166         MathEngine.init("localhost");

   167         MathEngine me = MathEngine.getMathEngine();

   169         IToCalc ct = me.getCalcTree(fmz);

   170         IToUser user = new MockIToUser();

   171         ct.addDataChangeListener(user);

   172         CalcChanged cce = null;

   173         System.out.println(".end step_a-----");

   174         //end step_a

   175         // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   177         ct.completeCalcHead();

   178         ICalcIterator ci = ct.getActiveFormula();

   179         CalcHead ch = (CalcHead) ci.getFormula();

   180         System.out.println(".end step_b-----");

   181         //end step_b

   182         // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   184         //let calculate the first formula

   185         Tactic tac = ct.fetchProposedTactic();

   186         //sent to bridge: fetchProposedTactic 1;

   187         System.out.println(".2nd tac:" + tac.toSMLString());

   188         assertEquals("mini-step: 2nd form", tac.toSMLString(),

   189                 "Apply_Method [\"Test\",\"squ-equ-test-subpbl1\"]");

   190         ct.setNextTactic(tac);

   191         //sent to bridge: setNextTactic 1

   192         // (Apply_Method["Test","squ-equ-test-subpbl1"]);

   193         ct.autoCalculate(IToCalc.SCOPE_CALCULATION,1);

   195         cce = ((MockIToUser) user).getCalcChangedEvent();

   196         assertEquals("unchanged", cce.getLastUnchangedFormula().toSMLString(),

   197                 "([],Met)");

   198         assertEquals("deleted", cce.getLastDeletedFormula().toSMLString(),

   199                 "([],Met)");

   200         assertEquals("generated", cce.getLastGeneratedFormula().toSMLString(),

   201                 "([1],Frm)");

   203         Vector elems = ci.getFormulaeFromTo(cce.getLastGeneratedFormula(),

   204                 new Integer(2), false);

   205         CalcFormula fa = (CalcFormula) (elems.firstElement());

   206         System.out.println(".2nd form: " + fa.toSMLString());

   207         assertEquals("mini-auto: 2nd form", fa.toSMLString(), "x + 1 = 2");

   209         System.out.println(".end step_c-----");

   210         //end step_c

   211         // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   213         //let calculate the second formula

   214         tac = ct.fetchProposedTactic();

   215         System.out.println(".3rd tac: " + tac.toSMLString());

   216         assertEquals("mini-step: 3rd tac", tac.toSMLString(),

   217                 "Rewrite_Set \"norm_equation\"");

   219         ct.setNextTactic(tac);

   220         //sent to bridge: autoCalculate 5 (Step 1);

   221         ct.autoCalculate(IToCalc.SCOPE_CALCULATION,1);

   222         cce = ((MockIToUser) user).getCalcChangedEvent();

   223         assertEquals("unchanged", cce.getLastUnchangedFormula().toSMLString(),

   224                 "([1],Frm)");

   225         assertEquals("deleted", cce.getLastDeletedFormula().toSMLString(),

   226                 "([1],Frm)");

   227         assertEquals("generated", cce.getLastGeneratedFormula().toSMLString(),

   228                 "([1],Res)");

   230         fa = (CalcFormula) (cce.getLastGeneratedFormula()).getElement();

   231         System.out.println(".3rd form: " + fa.toSMLString());

   232         assertEquals("mini-auto: 3rd form", fa.toSMLString(),

   233                 "x + 1 + -1 * 2 = 0");

   235         System.out.println(".end step_d-----");

   236         //end step_d

   237         // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   239         //set next a NOT applicable tactis (the one from above)

   240         ct.setNextTactic(tac);

   241         //cce = ((MockIToUser) user).getCalcChangedEvent();

   242         //.....WN050222 implicit autoCalculate disturbs the following step

   243         System.out.println(".end step_e-----");

   244         //end step_e

   245         // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   247         //.....WN050222 implicit autoCalculate disturbed the following step

   248         //WN050711 not restored according to corrected autoCalculate

   249         //			//let calculate the third formula

   250         //			tac = ct.fetchProposedTactic();

   251         //			assertEquals("mini-step: 4th tac", tac.toSMLString(),

   252         //					"Rewrite_Set \"Test_simplify\"");

   253         //

   254         //			ct.setNextTactic(tac);

   255         //			cce = ((MockIToUser) user).getCalcChangedEvent();

   256         //			//@@@@@error@@@error@@@error@@@error@@@error@@@----"([2],Res)"

   257         //			assertEquals("unchanged",

   258         // cce.getLastUnchangedFormula().toSMLString(),

   259         //					"([2],Res)");//"([1],Res)");...correct, but see

   260         //			// CalcTree#setNextTactic

   261         //			//@@@@@error@@@error@@@error@@@error@@@error@@@----"([2],Res)"

   262         //			assertEquals("deleted", cce.getLastDeletedFormula().toSMLString(),

   263         //					"([2],Res)");//"([1],Res)");...correct, but see

   264         //			// CalcTree#setNextTactic

   265         //			assertEquals("generated",

   266         // cce.getLastGeneratedFormula().toSMLString(),

   267         //					"([2],Res)");

   268         //

   269         //			fa = (CalcFormula) (cce.getLastGeneratedFormula()).getFormula();

   270         //			System.out.println(".4th form:" + fa.toSMLString());

   271         //			assertEquals("mini-auto: 4th form", fa.toSMLString(), "-1 + x = 0");

   272         //

   273         //			System.out.println(".end step_f-----");

   274         //			//end step_f

   275         //			//

   276         // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   277     }

   279     /**

   280      * uses the example 'IsacCore/Tests/minipbl_with_mini-subpbl'; comprises the

   281      * usecase UC\label{SOLVE:INFO:intermediate-steps} see

   282      * smltest/FE-interface/interface.sml "interSteps: on 'miniscript with

   283      * mini-subpbl'"

   284      */

   285     public void testIntermediateSteps() throws Exception {

   286         System.out

   287                 .println("---BEGIN isac.bridge.TestBridgeInput#testIntermediateSteps");

   289         //load the file of the example,

   290         //see TestKEStoreServices#testLoadContentMinisubpbl

   291         KEStoreServices ks = new KEStoreServices("isac/xmldata");

   292         Vector vec = ks.loadContent("exp", "exp_IsacCore_Tests_1b.xml");

   293         //parse out the Formalization

   294         //see TestFormalizationDigest#testParseExplMini

   295         String xmlstr = (String) vec.firstElement();

   296         FormalizationDigest fd = new FormalizationDigest();

   297         Formalization fmz = fd.parseFormalization((String) xmlstr);

   298         System.out.println(".end step_a-----");

   300         //start the calculation

   301         MathEngine.init("localhost");

   302         MathEngine me = MathEngine.getMathEngine();

   304         IToCalc ct = me.getCalcTree(fmz);

   305         IToUser user = new MockIToUser();

   306         ct.addDataChangeListener(user);

   307         CalcChanged cce = null;

   308         System.out.println(".end step_a-----");

   309         //end step_a

   310         // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   312         ct.autoCalculate(IToCalc.SCOPE_CALCULATION, 0);

   313         // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   315         // intermediateSteps(([2],Res)) gives 6 new steps

   316         Position pos = new Position();//([2],Res)

   317         pos.addInt("2");

   318         pos.setKind("Res");

   319         ICalcIterator ci = new CalcIterator((CalcTree) ct, pos);

   321         ct.intermediateSteps(ci);

   322         cce = ((MockIToUser) user).getCalcChangedEvent();

   323         Vector elems = cce.getLastUnchangedFormula().getFormulaeFromTo(

   324                 cce.getLastGeneratedFormula(), new Integer(3), false);

   325         CalcFormula fch = null;

   326         for (int i = 0; i < elems.size(); i++) {

   327             fch = (CalcFormula) elems.elementAt(i);

   328                 System.out.println(".step " + i + ": "

   329                         + ((CalcFormula) fch).getPosition().toSMLString() + " "

   330                         + fch.toSMLString());

   331         }

   332         System.out.println(".-------");

   333         assertEquals("mini-auto: steps= ", elems.size(), 7);

   334         assertEquals("mini-auto: first step", ((ICalcElement) elems

   335                 .firstElement()).toSMLString(), "x + 1 + -1 * 2 = 0");

   336         assertEquals("mini-auto: last step", ((ICalcElement) elems

   337                 .lastElement()).toSMLString(), "-1 + x = 0");

   339         // intermediateSteps(([3,2],Res)) gives 3 new steps

   340         pos = new Position();//([3,2],Res)

   341         pos.addInt("3");

   342         pos.addInt("2");

   343         pos.setKind("Res");

   344         ci = new CalcIterator((CalcTree) ct, pos);

   346         ct.intermediateSteps(ci);

   347         cce = ((MockIToUser) user).getCalcChangedEvent();

   348         elems = cce.getLastUnchangedFormula().getFormulaeFromTo(

   349                 cce.getLastGeneratedFormula(), new Integer(3), false);

   350         fch = null;

   351         for (int i = 0; i < elems.size(); i++) {

   352             fch = (CalcFormula) elems.elementAt(i);

   353                 System.out.println(".step " + i + ": "

   354                         + ((CalcFormula) fch).getPosition().toSMLString() + " "

   355                         + fch.toSMLString());

   356         }

   357         System.out.println(".-------");

   358         assertEquals("mini-auto: steps= ", elems.size(), 3);

   359         assertEquals("mini-auto: first step", ((ICalcElement) elems

   360                 .firstElement()).toSMLString(), "x = 0 + -1 * -1");

   361         assertEquals("mini-auto: last step", ((ICalcElement) elems

   362                 .lastElement()).toSMLString(), "x = 1");

   364         // intermediateSteps(([3],Res)) on CalcHead gives NO new steps

   365         pos = new Position();//([3],Res)

   366         pos.addInt("3");

   367         pos.setKind("Res");

   368         ci = new CalcIterator((CalcTree) ct, pos);

   370         ct.intermediateSteps(ci);

   371         cce = ((MockIToUser) user).getCalcChangedEvent();

   372         elems = cce.getLastUnchangedFormula().getFormulaeFromTo(

   373                 cce.getLastGeneratedFormula(), new Integer(1), false);

   374         fch = null;

   375         for (int i = 0; i < elems.size(); i++) {

   376             fch = (CalcFormula) elems.elementAt(i);

   377                 System.out.println(".step " + i + ": "

   378                         + ((CalcFormula) fch).getPosition().toSMLString() + " "

   379                         + fch.toSMLString());

   380         }

   381         System.out.println(".-------");

   382         assertEquals("mini-auto: steps= ", elems.size(), 3);

   383         assertEquals("mini-auto: first step", ((ICalcElement) elems

   384                 .firstElement()).toSMLString(), "-1 + x = 0");

   385         assertEquals("mini-auto: last step", ((ICalcElement) elems

   386                 .lastElement()).toSMLString(), "x = 1");

   388         // intermediateSteps(([],Res)) gives whole calctree (on 1st level)

   389         pos = new Position();//([],Res)

   390         pos.setKind("Res");

   391         ci = new CalcIterator((CalcTree) ct, pos);

   393         ct.intermediateSteps(ci);

   394         cce = ((MockIToUser) user).getCalcChangedEvent();

   395         elems = cce.getLastUnchangedFormula().getFormulaeFromTo(

   396                 cce.getLastGeneratedFormula(), new Integer(1), false);

   397         fch = null;

   398         for (int i = 0; i < elems.size(); i++) {

   399             fch = (CalcFormula) elems.elementAt(i);

   400                 System.out.println(".step " + i + ": "

   401                         + ((CalcFormula) fch).getPosition().toSMLString() + " "

   402                         + fch.toSMLString());

   403         }

   404         assertEquals("mini-auto: steps= ", elems.size(), 6);

   405         assertEquals("mini-auto: first step", ((ICalcElement) elems

   406                 .firstElement()).toSMLString(), "x + 1 = 2");

   407         assertEquals("mini-auto: last step", ((ICalcElement) elems

   408                 .lastElement()).toSMLString(), "[x = 1]");

   409     }

   411     /**

   412      * uses the example 'IsacCore/Tests/minipbl_with_mini-subpbl'; comprises the

   413      * UC\label{SOLVE:HIDE:getTactic} and UC\label{SOLVE:MANUAL:TACTIC:listall}

   414      * see smltest/FE-interface/interface.sml '- getTactic, fetchApplicableTactics -'

   415      */

   416     public void testTactics() throws Exception {

   417         System.out.println("---BEGIN isac.bridge.TestBridge#testTactics");

   419         //load the file of the example,

   420         //see TestKEStoreServices#testLoadContentMinisubpbl

   421         KEStoreServices ks = new KEStoreServices("isac/xmldata");

   422         Vector vec = ks.loadContent("exp", "exp_IsacCore_Tests_1b.xml");

   423         //parse out the Formalization

   424         //see TestFormalizationDigest#testParseExplMini

   425         String xmlstr = (String) vec.firstElement();

   426         FormalizationDigest fd = new FormalizationDigest();

   427         Formalization fmz = fd.parseFormalization((String) xmlstr);

   428         System.out.println(".end step_a-----");

   430         //start the calculation

   431         MathEngine.init("localhost");

   432         MathEngine me = MathEngine.getMathEngine();

   434         IToCalc ct = me.getCalcTree(fmz);

   435         IToUser user = new MockIToUser();

   436         ct.addDataChangeListener(user);

   437         CalcChanged cce = null;

   438         System.out.println(".end step_a-----");

   439         //end step_a

   440         // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   442         ct.autoCalculate(IToCalc.SCOPE_CALCULATION, 0);

   443         // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   445         // on (root) CalcHead: also with getApplicableTactics only one Tactic

   446         Position pos = new Position();//([],Pbl)

   447         pos.setKind("Pbl");

   448         ICalcIterator ci = new CalcIterator((CalcTree) ct, pos);

   450         Tactic tac = ci.getTactic();// <--------------------------------

   451         assertEquals("at ([],Pbl) found: ", ((Tactic) tac).toSMLString(),

   452                 "Apply_Method [\"Test\",\"squ-equ-test-subpbl1\"]");

   454         Vector tacs = ci.getApplicableTactics(99999);// <---------------

   455         assertEquals(((Tactic) tacs.firstElement()).toSMLString(),

   456                 "Apply_Method [\"Test\",\"squ-equ-test-subpbl1\"]");

   457         assertEquals("number of appl. tacs = ", tacs.size(), 1);

   459         // somewhere in rootproblem: all Tactics in the method

   460         pos = new Position();//([1],Res)

   461         pos.addInt("1");

   462         pos.setKind("Res");

   463         ci = new CalcIterator((CalcTree) ct, pos);

   465         tac = ci.getTactic();// <---------------------------------------

   466         assertEquals(tac.toSMLString(), "Rewrite_Set \"Test_simplify\"");

   468         tacs = ci.getApplicableTactics(99999);// <----------------------

   469         System.out.println(".at " + ci.toSMLString() + ":");

   470         for (int i = 0; i < tacs.size(); i++)

   471             System.out.println(".." + ((Tactic) tacs.get(i)).toSMLString());

   472         assertEquals("number of appl. tacs = ", tacs.size(), 3);

   474         // on CalcHead of subproblem: only Apply_Method

   475         pos = new Position();//([3],Pbl)

   476         pos.addInt("3");

   477         pos.setKind("Pbl");

   478         ci = new CalcIterator((CalcTree) ct, pos);

   480         tac = ci.getTactic();// <---------------------------------------

   481         assertEquals(tac.toSMLString(),

   482                 "Apply_Method [\"Test\",\"solve_linear\"]");

   484         tacs = ci.getApplicableTactics(99999);// <----------------------

   485         assertEquals("at ([3],Pbl) found: ", ((Tactic) tacs.firstElement())

   486                 .toSMLString(), "Apply_Method [\"Test\",\"solve_linear\"]");

   487         assertEquals("number of appl. tacs = ", tacs.size(), 1);

   489         // somewhere in subproblem: all Tactics in this (other) method

   490         pos = new Position();//([3,1],Res)

   491         pos.addInt("3");

   492         pos.addInt("1");

   493         pos.setKind("Res");

   494         ci = new CalcIterator((CalcTree) ct, pos);

   496         tac = ci.getTactic();// <---------------------------------------

   497         assertEquals(tac.toSMLString(), "Rewrite_Set \"Test_simplify\"");

   499         tacs = ci.getApplicableTactics(99999);// <----------------------

   500         System.out.println(".at " + ci.toSMLString() + ":");

   501         for (int i = 0; i < tacs.size(); i++)

   502             System.out.println(".." + ((Tactic) tacs.get(i)).toSMLString());

   503         assertEquals("at ([3,1],Res) found: ", tacs.size(), 3);

   505         // on the result of the subproblem again all tacs of the rootpbl

   506         pos = new Position();//([3],Res)

   507         pos.addInt("3");

   508         pos.setKind("Res");

   509         ci = new CalcIterator((CalcTree) ct, pos);

   511         tac = ci.getTactic();// <---------------------------------------

   512         assertEquals(tac.toSMLString(), "Check_elementwise \"Assumptions\"");

   514         tacs = ci.getApplicableTactics(99999);// <----------------------

   515         System.out.println(".at " + ci.toSMLString() + ":");

   516         for (int i = 0; i < tacs.size(); i++)

   517             System.out.println(".." + ((Tactic) tacs.get(i)).toSMLString());

   518         assertEquals("at ([3],Res) found: ", tacs.size(), 1);

   520         // but on the final result there are _NO_ tacs applicable

   521         pos = new Position();//([],Res)

   522         pos.setKind("Res");

   523         ci = new CalcIterator((CalcTree) ct, pos);

   524         // tac = ci.getTactic();// <------------------------------------

   525         // tacs = ci.getApplicableTactics(99999);// <-------------------

   526         // TODO handle error msg

   527     }

   529     /**

   530      * uses the example 'IsacCore/Tests/rat.equ, asms'; comprises the usecases

   531      * UC\label{SOLVE:HELP:assumptions} and

   532      * *UC\label{SOLVE:HELP:assumptions-origin} smltest/FE-interface/interface.sml '-

   533      * getAssumptions, getAccumulatedAsms -'

   534      */

   535     public void testAssumptions() throws Exception {

   536         System.out.println("---BEGIN isac.bridge.TestBridge#testAssumptions");

   538         //load the file of the example,

   539         //see TestKEStoreServices#testLoadContentMinisubpbl

   540         KEStoreServices ks = new KEStoreServices("isac/xmldata");

   541         Vector vec = ks.loadContent("exp", "exp_IsacCore_Tests_1c.xml");

   542         //parse out the Formalization

   543         //see TestFormalizationDigest#testParseExplMini

   544         String xmlstr = (String) vec.firstElement();

   545         FormalizationDigest fd = new FormalizationDigest();

   546         Formalization fmz = fd.parseFormalization((String) xmlstr);

   547         System.out.println(".end step_a-----");

   549         //start the calculation

   550         MathEngine.init("localhost");

   551         MathEngine me = MathEngine.getMathEngine();

   553         IToCalc ct = me.getCalcTree(fmz);

   554         IToUser user = new MockIToUser();

   555         ct.addDataChangeListener(user);

   556         CalcChanged cce = null;

   557         System.out.println(".end step_a-----");

   558         //end step_a

   559         // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

   561         ct.autoCalculate(IToCalc.SCOPE_CALCULATION, 0);

   563         //		for (int i = 0; i < forms.size(); i++)

   564         //			System.out.println(".asm= "

   565         //					+ ((Formula) forms.elementAt(i)).toSMLString());

   567         // here the assumption arises

   568         Position pos = new Position();//([3],Res)

   569         pos.addInt("3");

   570         pos.setKind("Res");

   571         CalcIterator ci = new CalcIterator((CalcTree) ct, pos);

   573         Assumptions asm = ci.getAssumptions();//<---------------------------

   574         Vector forms = asm.getFormulae();

   575         assertEquals("asm generated here:", ((Formula) forms.firstElement())

   576                 .toSMLString(), "9 * x + -6 * x ^ 2 + x ^ 3 ~= 0");

   577         asm = ci.getAccumulatedAssumptions();//<----------------------------

   578         forms = asm.getFormulae();

   579         assertEquals("is the only asm:", ((Formula) forms.firstElement())

   580                 .toSMLString(), "9 * x + -6 * x ^ 2 + x ^ 3 ~= 0");

   582         // here the assumption is checked

   583         pos = new Position();//([5],Res)

   584         pos.addInt("5");

   585         pos.setKind("Res");

   586         ci = new CalcIterator((CalcTree) ct, pos);

   588         asm = ci.getAssumptions();//<---------------------------------------

   589         forms = asm.getFormulae();

   590         assertEquals("here no asm generated:", forms.size(), 0);

   591         asm = ci.getAccumulatedAssumptions();//<----------------------------

   592         forms = asm.getFormulae();

   593         assertEquals("acumulated from above:", ((Formula) forms.firstElement())

   594                 .toSMLString(), "9 * x + -6 * x ^ 2 + x ^ 3 ~= 0");

   596         System.out.println("---END isac.bridge.TestBridge");

   597     }

   599 }

author	wneuper
	Thu, 21 Feb 2008 14:19:57 +0100
changeset 3893	c6e6c271ee07
parent 3881	72f0be16d83b
child 3928	d38196e9b162
permissions	-rw-r--r--