Logo Search packages:      
Sourcecode: tcm version File versions  Download package

stdiagram.c

////////////////////////////////////////////////////////////////////////////////
//
// This file is part of Toolkit for Conceptual Modeling (TCM).
// (c) copyright 2001, Universiteit Twente.
// Author: Frank Dehne (frank@cs.vu.nl), David N. Jansen (dnjansen@cs.utwente.nl)
//
// TCM is free software; you can redistribute it and/or modify
// it under the terms of the GNU General Public License as published by
// the Free Software Foundation; either version 2 of the License, or
// (at your option) any later version.
//
// TCM is distributed in the hope that it will be useful,
// but WITHOUT ANY WARRANTY; without even the implied warranty of
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
// GNU General Public License for more details.
//
// You should have received a copy of the GNU General Public License
// along with TCM; if not, write to the Free Software
// Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
// 02111-1307, USA.
////////////////////////////////////////////////////////////////////////////////
#include "stgraph.h"
#include "stviewer.h"
#include "stwindow.h"
#include "stchecks.h"
#include "messagedialog.h"
#include "replacedialog.h"
#include "initialstate.h"
#include "decisionpoint.h"
#include "transition.h"
#include "hexagon.h"
#include "textbox.h"
#include "comment.h"
#include "transitionarrow.h"
#include "initialstatebox.h"
#include "stdiagram.h"
#include "editstubs.h"
#include "system.h"
#include "printer.h"
#include <limits.h>

#ifdef MODELCHECK

#define MODELCHECK_SMV 1

#include "modelcheckdialog.h"

#if MODELCHECK_SMV
      #include "smv.h"
#else
      #include "kronos.h"
#endif

#include <stdlib.h>
#include <ctype.h>
#include <stdio.h>
#endif

const int STDiagram::BOX_WIDTH = 100;
const int STDiagram::BOX_HEIGHT = 38;
 
STDiagram::STDiagram(Config *c, STWindow *d, STViewer *v, STGraph *g): 
            Diagram(c,d,v,g) {
      UpdateNodeType(1);
      UpdateEdgeType(1);
      GetReplaceDialog()->ManageNameOnlyToggle(True);
      stChecks = new STChecks(this,g);
#ifdef MODELCHECK
      promptDialog = new ModelCheckDialog(GetMainWindow()->GetWidget());
      promptDialog->Initialize();
#endif
}


STDiagram::~STDiagram() {
#ifdef MODELCHECK
      delete promptDialog;
#endif
      delete stChecks;
}


00083 Thing *STDiagram::CreateThing(int classNr) {
      Grafport *g = GetDiagramViewer()->GetGrafport();
      ShapeView *v = GetDiagramViewer()->GetCurView();
      STGraph *sg = (STGraph *)GetGraph();
      Thing *thing = 0;
      // view
      if (classNr == Code::VIEW)
            thing = new ShapeView(GetDiagramViewer());
      // node shapes
      else if (classNr == Code::ARROW_BOX)
            thing = new InitialStateBox(v, g, 0, 0); 
      else if (classNr == Code::BOX)
            thing = new Box(v, g, 0, 0); 
      else if (classNr == Code::HEXAGON)
            thing = new Hexagon(v, g, 0, 0); 
      else if (classNr == Code::TEXT_BOX)
            thing = new TextBox(v, g, 0, 0); 
      // lines
      else if (classNr == Code::TRANSITION_ARROW)
            thing = new TransitionArrow(v, g, 0, 0, 0);
      // nodes
      else if (classNr == Code::INITIAL_STATE)
            thing = new InitialState(sg);
      else if (classNr == Code::STATE)
            thing = new State(sg);
      else if (classNr == Code::DECISION_POINT)
            thing = new DecisionPoint(sg);
      else if (classNr == Code::COMMENT)
            thing = new Comment(sg);
      // edges
      else if (classNr == Code::TRANSITION)
            thing = new Transition(sg, 0, 0);
      else 
            error("%s, line %d: impl error: "
                  "wrong class number %d\n", __FILE__, __LINE__, classNr);
      return thing;
}

00121 Node *STDiagram::CreateNode(){
      Node *node = 0;
      STGraph *sg = (STGraph *)GetGraph();
      if (GetNodeType() == Code::INITIAL_STATE)
            node = new InitialState(sg);
      else if (GetNodeType() == Code::STATE)
            node = new State(sg);
      else if (GetNodeType() == Code::DECISION_POINT)
            node = new DecisionPoint(sg);
      else if (GetNodeType() == Code::COMMENT)
            node = new Comment(sg);
      else
            error("%s, line %d: impl error: "
                  "unknown node type\n", __FILE__, __LINE__);
      return node;
}

00138 Edge *STDiagram::CreateEdge(Subject *subj1, Subject *subj2){
      if (!CheckEdgeConstraints(subj1, subj2))
            return 0; 
      Edge *edge = 0;
      STGraph *sg = (STGraph *)GetGraph();
      if (GetEdgeType() == Code::TRANSITION)
            edge = new Transition(sg, subj1, subj2);
      else
            error("%s, line %d: impl error: "
                  "unknown edge type\n", __FILE__, __LINE__);
      return edge;
}

00151 NodeShape *STDiagram::CreateNodeShape(Node *node, int x, int y) {
      NodeShape *shape = 0;
      Grafport *g = GetDiagramViewer()->GetGrafport();
      ShapeView *v = GetDiagramViewer()->GetCurView();
      if (GetNodeShapeType() == Code::ARROW_BOX)
            shape = new InitialStateBox(v, g, x, y);
      else if (GetNodeShapeType() == Code::BOX)
            shape = new Box(v, g, x, y);
      else if (GetNodeShapeType() == Code::HEXAGON)
            shape = new Hexagon(v, g, x, y);
      else if (GetNodeShapeType() == Code::TEXT_BOX)
            shape = new TextBox(v, g, x, y);
      else
            error("%s, line %d: impl error: "
                  "node shape type does not exist\n", __FILE__, __LINE__);
      if (check(shape)) {
            shape->SetSubject(node);
            shape->SetTextShape();
      }
      return shape;
}

00173 Line *STDiagram::CreateLine(
            Edge *edge, GShape *from, GShape *to, List<Point *> *l) {
      Line *line = 0;
      Grafport *g = GetDiagramViewer()->GetGrafport();
      ShapeView *v = GetDiagramViewer()->GetCurView();
      *((*l)[0]) = *(from->GetPosition());
      *((*l)[l->count()-1]) = *(to->GetPosition());
      if (GetLineType() == Code::TRANSITION_ARROW)
            line = new TransitionArrow(v, g, from, to, l, IsCurve());
      else
            error("%s, line %d: impl error: "
                  "line type does not exist\n", __FILE__, __LINE__);

      if (check(line)) {
            line->SetSubject(edge);
            line->SetTextShape();
      }
      return line;
}

00193 void STDiagram::UpdateNodeType(int num) {
      ((DiagramWindow *)GetMainWindow())->SetNodeName(num);
      switch (num) {
      case 1: SetNodeType(Code::INITIAL_STATE);
            SetNodeShapeType(Code::ARROW_BOX);
            break;
      case 2: SetNodeType(Code::STATE);
            SetNodeShapeType(Code::BOX);
            break;
      case 3: SetNodeType(Code::DECISION_POINT);
            SetNodeShapeType(Code::HEXAGON);
            break;
      case 4: SetNodeType(Code::COMMENT);
            SetNodeShapeType(Code::TEXT_BOX);
            break;
      default:
            error("%s, line %d: impl error: "
                  "unknown node type selected\n", __FILE__,__LINE__);
      }
}

00214 void STDiagram::UpdateEdgeType(int num) {
      ((DiagramWindow *)GetMainWindow())->SetEdgeName(num);
      switch(num) {
      case 1: SetEdgeType(Code::TRANSITION);
            SetLineType(Code::TRANSITION_ARROW);
            break;
      default:
            error("%s, line %d: impl error: "
                  "unknown edge type selected\n", __FILE__,__LINE__);
      }
}

bool STDiagram::CheckEdgeConstraints(Subject *subj1, Subject *subj2) {
      // Check possible connections (subj-subj-edge matrix).
      if (!CheckConnection(subj1, subj2))
            return False;
      // Check that two different initial states can't be connected.
      else if (subj1->GetClassType() == Code::INITIAL_STATE &&
             subj2->GetClassType() == Code::INITIAL_STATE && subj1 != subj2) {
             ShowDialog(MessageDialog::ERROR, "Error", 
                  "Cannot connect different initial states");
             return False;
      }
      // Check that a decision point can not be connected to itself.
      else if (subj1->GetClassType() == Code::DECISION_POINT && subj1 == subj2) {
             ShowDialog(MessageDialog::ERROR, "Error",
                  "Cannot connect a decision point with itself");
             return False;
      }

      // Check that two subjs are not reachable from different initial states.
      InitialState *init1, *init2;
      init1 = FindInitialState(subj1); init2 = FindInitialState(subj2);
      if (init1 && init2) {
            if (init1 != init2) {
                  ShowDialog(MessageDialog::ERROR, "Error",
                        "Cannot connect nodes from different STDs");
                  return False;
            }
      }
      return True;
}

bool STDiagram::SetEvent(Transition *t, const string *s) {
      List<GShape *> shapes;
      GetDiagramViewer()->GetShapes(t, &shapes);
      Subject::NameErrType n = t->SetEvent(s);
      if (n == Subject::OK) {
            if (shapes.first())
                  do
                        ((TransitionArrow *)shapes.cur())->UpdateEvent(s);
                  while (shapes.next());
            else {
                  error("%s, line %d: shape does not exist\n", 
                              __FILE__, __LINE__);
                  return False;
            }
            return True;
      }
      else if (n == Subject::IMPOSSIBLE_NAME) {
            string msg = "'" + *s + "' wrong syntax\n for an event string";
            ShowDialog(MessageDialog::ERROR, "Error", &msg);
            return False;
      }
      else if (n == Subject::DOUBLE_EDGE) {
            string msg = "there is already a transition with\n"
                  "event string '" + *s + "' between this pair of states";
            ShowDialog(MessageDialog::ERROR, "Error", &msg);
            return False;
      }
      else {
            error("%s, line %d: case not handled\n", __FILE__, __LINE__);
      }
      return True;
}

bool STDiagram::SetAction(Subject *t, const string *s, unsigned nr) {
      List<GShape *> shapes;
      GetDiagramViewer()->GetShapes(t, &shapes);
      unsigned m = nr;
      // split string in different one line strings.
      string ss(*s);
      char *str = (char *)ss.getstr();
      char empty[2] = "";
      char *x = strtok(str, "\r");
      if (x == 0)
            x = empty;
      while (x != 0) {
            string *ns = new string(x);
            bool update = True;
            Subject::NameErrType result;
            if (m == nr) {
                  if (t->IsEdge())
                        result = ((Transition *)t)->SetAction(ns, m, True);
                  else
                        result = ((InitialState *)t)->SetAction(ns, m, True);
            }
            else {
                  if (t->IsEdge())
                        result = ((Transition *)t)->SetAction(ns, m, False);
                  else
                        result = ((InitialState *)t)->SetAction(ns, m, False);
                  update = False;
            }
            if (result != Subject::OK) {
                  string msg;
                  if (result == Subject::HAS_ACTION)
                        msg = "transition already has an action '" + *ns + "'";
                  else
                        msg = "'" + *ns + "' wrong syntax\n for an action string";
                  ShowDialog(MessageDialog::ERROR, "Error", &msg);
                  // make actions empty.
                  *ns = "";
                  if (!update) {
                        for (shapes.first(); !shapes.done(); shapes.next()) {
                              if (t->IsEdge())
                                    ((TransitionArrow *)shapes.cur())->
                                          UpdateAction(ns, m, update);
                              else
                                    ((InitialStateBox *)shapes.cur())->
                                          UpdateAction(ns, m, update);
                        }
                  } 
                  delete ns;
                  return False;
            }
            // update the shapes.
            if (shapes.first())
                  do {
                        if (t->IsEdge())
                              ((TransitionArrow *)shapes.cur())->
                                    UpdateAction(ns, m, update);
                        else
                              ((InitialStateBox *)shapes.cur())->
                                    UpdateAction(ns, m, update);
                  } while (shapes.next());
            else {
                  error("%s, line %d: shape does not exist\n", 
                              __FILE__, __LINE__);
                  return False;
            }
            m++;
            x = strtok(0, "\r");
            delete ns;
      }
      return True;
}

InitialState *STDiagram::FindInitialState(Subject *state) {
      if (state->GetClassType() == Code::INITIAL_STATE)
            return (InitialState *)state;
      List<Subject *> initStates;
      GetGraph()->GetNodes(&initStates, Code::INITIAL_STATE);
      for (initStates.first(); !initStates.done(); initStates.next()) {
            InitialState *init = (InitialState *)initStates.cur();
            if (GetGraph()->UndirectedPathExists(init, state))
                  return init;
      } 
      return 0;
}

00375 void STDiagram::CheckDocument() {
      chkbuf = "";
      unsigned total = 0;
      total += stChecks->CheckNamelessNodes(Code::INITIAL_STATE, chkbuf);
      total += stChecks->CheckNamelessNodes(Code::STATE, chkbuf);
      total += stChecks->CheckNamelessNodes(Code::DECISION_POINT, chkbuf);
      total += stChecks->CheckDoubleNodes(Code::STATE, chkbuf);
      total += stChecks->CheckDoubleNodes(Code::DECISION_POINT, chkbuf);
      total += stChecks->CheckDoubleEvents(chkbuf);
      total += stChecks->CheckEmptyEvents(chkbuf);
      total += stChecks->CheckEmptyActions(chkbuf);
      total += stChecks->CheckNoActions(chkbuf);
      total += stChecks->CheckCountEdgesFrom(Code::DECISION_POINT, 
            Code::TRANSITION, 2, INT_MAX, False, False, chkbuf);
      int sub = stChecks->CheckNodeCount(1, Code::INITIAL_STATE, chkbuf);
      total += sub;
      if (sub == 0) {
            total += stChecks->CheckReachability(
                  Code::INITIAL_STATE, Code::STATE, False, chkbuf);
            total += stChecks->CheckReachability(
                  Code::INITIAL_STATE, Code::DECISION_POINT, False, chkbuf);
      }
      ReportCheck(total, &chkbuf);
}


#ifdef MODELCHECK
void STDiagram::ModelCheckProperty() {
      SetStatus("action: model check document semantics");
      promptDialog->SetTitle("Model check document semantics");
      promptDialog->SetOKCallback(ModelCheckDocumentOKCB, this);
      promptDialog->Popup();
}


/* static */ void STDiagram::ModelCheckDocumentOKCB(Widget,
            XtPointer clientData, XtPointer)
{
      STDiagram *std = (STDiagram *)clientData;
      string formula, internal, clock;
      std->promptDialog->GetFormulaString(&formula);
      std->promptDialog->GetInternString(&internal);
      std->promptDialog->GetClockString(&clock);
      std->DoModelCheckDocument(&internal, &formula, &clock);
}


void STDiagram::DoModelCheckDocument(const string *internal,
                  const string *formula, const string *clock)
{
      SetStatus("action: model check document semantics");
      GetMainWindow()->SetCursor(MouseCursor::WATCH);
      string tmpModel;
tmpModel = "model";
//    GetViewer()->GetPrinter()->MakeTmpFile(&tmpModel);
#if MODELCHECK_SMV
      tmpModel += ".smv";
#else
      tmpModel += ".tg";
#endif
std::cerr << "Temporary model file: " << tmpModel.getstr() << '\n';

      SaveForModelChecker(&tmpModel, internal, clock, formula);
      bool ok = ExecuteModelChecker(&tmpModel, formula);
      GetMainWindow()->SetCursor(MouseCursor::LEFT_PTR);
//    unlink(tmpModel.getstr());
      if ( ! ok )
            SetStatus("model checking aborted");
      else
            SetStatus("model checking completed");
      return;
}


void STDiagram::SaveForModelChecker(const string *path, const string *internal,
                  const string * clock, const string *formula) {
      /* Split internal into a list of strings */
      List<string> intevent;
      if ( internal ) {
            const char *cp = internal->getstr();
            while ( *cp ) {
                  while ( *cp && isspace(*cp) )
                        ++cp;
                  if ( ! *cp )
                        break;
                  const char *ep = cp;
                  if ( '[' == *cp ) {
                        while ( *++ep )
                              if ( ']' == *ep ) {
                                    ++ep;
                                    break;
                              }
                  } else
                        while ( *++ep && ! isspace(*ep) && '[' != *ep )
                              ;
                  string event;
                  event.add(cp, ep - cp);
                  intevent.add(event);
                  cp = ep;
            }
      }

#if MODELCHECK_SMV
      SMV s(GetGraph());
      s.WriteSMV(path->getstr(), &intevent, formula);
#else
      Kronos kr(this);
      kr.GenerateKronos(&intevent);
      kr.SaveKronos(path->getstr(), clock->getstr());
#endif
}


bool STDiagram::ExecuteModelChecker(const string *path, const string *formula) {
#if MODELCHECK_SMV
      return False;
#else
      string tmpFormula;
tmpFormula = "/home/maics/dnjansen/kronos/formula";
//    GetViewer()->GetPrinter()->MakeTmpFile(&tmpFormula);
      tmpFormula += ".tctl";
      FILE *fp;
      if ( (fp = fopen(tmpFormula.getstr(), "w")) == NULL ||
          fputs(formula->getstr(), fp) == EOF ) {
            string txt("error, ");
            txt += tmpFormula;
            txt += "\ncannot be written";
            (new MessageDialog(GetMainWindow()->GetWidget(), 
                  MessageDialog::INFORMATION))->
                  Show("Notice", &txt);
            return False;
      }
      fclose(fp);
      string command;
command = "/home/maics/dnjansen/kronos/bin/kronos";
//    read config...
      command += " -v -reach ";
      command += tmpFormula;
      command += ' ';
      command += *path;
      int status = system(command.getstr());
//    unlink(tmpFormula.getstr());
      if (status) {
            string txt = "error, " + command;
            txt += "\ncannot be executed";
            (new MessageDialog(GetMainWindow()->GetWidget(), 
                  MessageDialog::INFORMATION))->
                  Show("Notice", &txt);
            return False;
      }
      return True;
#endif
}
#endif


00531 bool STDiagram::SetText(TextShape *t, const string *s) {
      const string *description = t->GetDescription();
      Subject *subj = t->GetParent()->GetSubject();
      if (*description == "Event")
            return SetEvent((Transition *)subj, s);
      else if (*description == "Action")
            return SetAction(subj, s, t->GetSequence());
      else 
            return Diagram::SetText(t, s);
}

Generated by  Doxygen 1.6.0   Back to index