#include "ioInt.h"

Include dependency graph for ioWriteSmv.c:

Functions
void	Io_SmvPrintVar (FILE fp, Var_Variable_t var)
void	IoSmvWrite (FILE fp, Hrc_Manager_t hmgr)
void	IoSmvPrint (FILE fp, Var_Variable_t var)
void	IoSmvPrintSpecial (FILE fp, Var_Variable_t var)

Function Documentation

void Io_SmvPrintVar	(	FILE *	fp,
		Var_Variable_t *	var
	)

CFile***********************************************************************

FileName [ioWriteSmv.c]

PackageName [io]

Synopsis [Writes out an Smv file.]

Description [Write the current model to a file compatible with NuSMV v2.1]

Author [Daniel Sheridan, Chao Wang]

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.]AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Prints out variable name, cleaned for NuSMV]

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file ioWriteSmv.c.

{
  char * varname = Var_VariableReadName(var);
  int i;

  for(i=0; varname[i]; i++) {
    if(varname[i] == '<' || 
       varname[i] == '>' || 
       varname[i] == '*' || 
       varname[i] == '$') {
      fputc('_', fp);
    } else {
      fputc(varname[i], fp);
    }
  }
}

Here is the call graph for this function:

Here is the caller graph for this function:

void IoSmvPrint	(	FILE *	fp,
		Var_Variable_t *	var
	)

Function********************************************************************

Synopsis [Prints out VAR declaration for a given variable.]

Description [Prints out VAR declaration for a given variable.]

SideEffects []

SeeAlso []

Definition at line 157 of file ioWriteSmv.c.

{
  int is_enum, range, i;

  is_enum = Var_VariableTestIsEnumerative(var);
  range = Var_VariableReadNumValues(var);
    
  if (is_enum == 1){
    if (range == 2){
      (void)fprintf(fp,"VAR %s : boolean;\n",Var_VariableReadName(var));
    }
    else {
      (void)fprintf(fp,"VAR %s : 0..%d;\n",Var_VariableReadName(var),range-1);
    }
  }
  else {
  /* variable var is symbolic */
    (void)fprintf(fp,"VAR %s : {",Var_VariableReadName(var));
    for (i=0; i < range; i++){
      if (i == (range-1))
        (void)fprintf(fp,"%s ",Var_VariableReadSymbolicValueFromIndex(var,i));
      else
        (void)fprintf(fp,"%s, ",Var_VariableReadSymbolicValueFromIndex(var,i));
    }
    (void)fprintf(fp,"};\n");
  }
}

Here is the call graph for this function:

void IoSmvPrintSpecial	(	FILE *	fp,
		Var_Variable_t *	var
	)

Function********************************************************************

Synopsis [Prints out VAR declaration for a given variable, with the special string "_bufin" appended to the variable name.]

Description [Prints out VAR declaration for a given variable.]

SideEffects []

SeeAlso []

Definition at line 200 of file ioWriteSmv.c.

{
  int is_enum, range, i;

  is_enum = Var_VariableTestIsEnumerative(var);
  range = Var_VariableReadNumValues(var);
    
  if (is_enum == 1){
    if (range == 2){
      (void)fprintf(fp,"VAR %s_bufin : boolean;\n",Var_VariableReadName(var));
    }
    else {
      (void)fprintf(fp,"VAR %s_bufin : 0..%d;\n",Var_VariableReadName(var),
                    range-1);
    }
  }
  else {
  /* variable var is symbolic */
    (void)fprintf(fp,"VAR %s_bufin : {",Var_VariableReadName(var));
    for (i=0; i < range; i++){
      if (i == (range-1)) 
        (void)fprintf(fp,"%s_bufin ",
                      Var_VariableReadSymbolicValueFromIndex(var,i));
      else
        (void)fprintf(fp,"%s_bufin, ",
                      Var_VariableReadSymbolicValueFromIndex(var,i));
    }
    (void)fprintf(fp,"};\n");
  }
}

Here is the call graph for this function:

void IoSmvWrite	(	FILE *	fp,
		Hrc_Manager_t *	hmgr
	)

Function********************************************************************

Synopsis [The top-level routine for writing out an NuSMV file.]

Description [The top-level routine for writing out an NuSMV file. The user has to check if the hmgr has a hierarchy read in before calling this procedure.]

SideEffects []

SeeAlso []

Definition at line 115 of file ioWriteSmv.c.

{ 
  char *rootModelName;
  Hrc_Model_t *model, *rootModel;
  Hrc_Node_t *currentNode;
  array_t *models;
  int i;
  boolean isRootModel;
  char *rootInstanceName, *instanceName;
  
  currentNode = Hrc_ManagerReadCurrentNode(hmgr);
  models = Hrc_ManagerObtainComponentModels(hmgr);

  rootModelName = Hrc_NodeReadModelName(currentNode);
  rootModel = Hrc_ManagerFindModelByName(hmgr,rootModelName);
  rootInstanceName = Hrc_NodeReadInstanceName(currentNode);
  assert(rootModel != NIL(Hrc_Model_t));
  
  for (i=0; i < array_n(models); i++){
    model = array_fetch(Hrc_Model_t *,models,i);
    isRootModel = (model == rootModel) ? TRUE : FALSE;
    instanceName = (isRootModel == TRUE) ? rootInstanceName : NIL(char);
    Hrc_ModelWriteSmv(fp,model,isRootModel,instanceName);
  }  

  array_free(models);
}

Here is the call graph for this function:

Here is the caller graph for this function:

src/io/ioWriteSmv.c File Reference

Functions

Function Documentation