CoreLibraryTutorial.cpp

// Basic C++ libraries
#include <iostream>
#include <string>
#include <sstream>
 
using namespace std;
 
// Core libraries 
#include "mcrl2/core/messaging.h"           // Messaging library
#include "mcrl2/core/parse.h"               // Parse library
#include "mcrl2/core/typecheck.h"           // Type check library
#include "mcrl2/core/data_implementation.h" // Data implementation library
#include "mcrl2/core/alpha.h"               // Alphabet reduction library
 
// Core/detail libraries 
#include "mcrl2/core/detail/struct.h"       // ATerm building blocks
 
using namespace mcrl2::core;                // core-namespace
using namespace mcrl2::core::detail;        // core::detail-namespace
 
std::string spec =
"act a: Bool;                    \n"
"init a(true);                   \n";
 
int main(int argc, char **argv)
{
 
  MCRL2_ATERM_INIT(argc, argv)   // initialise ATerm library
 
  gsSetVerboseMsg();             // enable Verbose logging 
 
  istringstream istr( spec );    // convert string to stringstream
 
  ATermAppl parsed_spec = parse_proc_spec( istr );
  if (parsed_spec == NULL) 
  {
    gsErrorMsg("parsing failed\n");
    return 1;
  }
  gsVerboseMsg("parsing succeeded!\n");
 
  ATermAppl typed_checked_parsed_spec = type_check_proc_spec( parsed_spec );
  if (typed_checked_parsed_spec == NULL) 
  {
    gsErrorMsg("type checking failed!\n");
    return 1;
  }
  gsVerboseMsg("type checking succeeded!\n");
 
  gsVerboseMsg("pretty printed specification:\n%P\n", typed_checked_parsed_spec );
  gsVerboseMsg("textual ATerm representation of the specification\n%T\n", typed_checked_parsed_spec );
 
  ATermAppl data_impl_typed_checked_parsed_spec = implement_data_proc_spec( typed_checked_parsed_spec );
  if (data_impl_typed_checked_parsed_spec == NULL) 
  {
    gsErrorMsg("data implementation failed\n");
    return 1;
  }
  gsVerboseMsg("data implementation succeeded!\n");
 
  gsDebugMsg("pretty printed specification:\n%P\n", data_impl_typed_checked_parsed_spec );
 
  assert( gsIsSpecV1( data_impl_typed_checked_parsed_spec ) );
 
  ATermAppl actIdB = gsMakeActSpec( ATmakeList1( (ATerm) gsMakeActId( gsString2ATermAppl("b"), ATmakeList0() ) ) );
 
  ATermAppl actB = gsMakeAction( (ATermAppl) ATgetFirst( ATgetArgument(actIdB, 0 ) ), ATmakeList0() );
 
  ATermAppl init = gsMakeProcessInit( ATmakeList0(), actB );
 
  ATermAppl new_spec = gsMakeSpecV1( 
                           ATAgetArgument(data_impl_typed_checked_parsed_spec, 0 )
                         , actIdB 
                         , ATAgetArgument(data_impl_typed_checked_parsed_spec, 2 )
                          , init 
                        ); 
 
  gsVerboseMsg("pretty printed version of the specification:\n%P", new_spec );
 
  ATermAppl new_alpha_spec = gsAlpha( new_spec );
 
  assert( gsIsSpecV1( new_alpha_spec ) );
 
  return 0;
}