diff --git a/ctx_aut.cc b/ctx_aut.cc index b51d2de..38030dd 100644 --- a/ctx_aut.cc +++ b/ctx_aut.cc @@ -40,9 +40,23 @@ void CtxAut::addState(std::string name) states_ids.push_back(name); states_names[name] = new_state_id; + + if (!init_state_defined) + { + setInitState(name); + } } } +void CtxAut::setInitState(std::string name) +{ + VERB_L2("Setting initial CA state: " << name); + State state_id = getStateID(name); + VERB_L2("Got initial CA state ID: index=" << state_id); + init_state_id = state_id; + init_state_defined = true; +} + void CtxAut::printAutomaton(void) { showStates(); @@ -52,6 +66,7 @@ void CtxAut::printAutomaton(void) void CtxAut::showStates(void) { cout << "# Context Automaton States:" << endl; + cout << " = Init state: " << getStateName(init_state_id) << endl; for (const auto &s : states_ids) cout << " * " << s << endl; } diff --git a/ctx_aut.hh b/ctx_aut.hh index fe08848..7c81aa1 100644 --- a/ctx_aut.hh +++ b/ctx_aut.hh @@ -31,6 +31,7 @@ class CtxAut CtxAut(Options *opts, RctSys *parent_rctsys); bool hasState(std::string name); void addState(std::string stateName); + void setInitState(std::string stateName); State getStateID(std::string name); std::string getStateName(State state_id); void printAutomaton(void); @@ -45,6 +46,8 @@ class CtxAut Options *opts; StatesById states_ids; StatesByName states_names; + State init_state_id; + bool init_state_defined; Entities tmpEntities; Transitions transitions; }; diff --git a/rs.cc b/rs.cc index 4ce6a67..7ccacf3 100644 --- a/rs.cc +++ b/rs.cc @@ -190,15 +190,21 @@ void RctSys::ctxAutAddState(std::string stateName) ctx_aut->addState(stateName); } +void RctSys::ctxAutSetInitState(std::string stateName) +{ + assert(ctx_aut != nullptr); + ctx_aut->setInitState(stateName); +} + void RctSys::ctxAutAddTransition(std::string srcStateName, std::string dstStateName) { assert(ctx_aut != nullptr); ctx_aut->addTransition(srcStateName, dstStateName); } -void RctSys::ctxAutPushNamedContextEntity(std::string entity_name) +void RctSys::ctxAutPushNamedContextEntity(std::string entityName) { assert(ctx_aut != nullptr); - Entity entity_id = getEntityID(entity_name); + Entity entity_id = getEntityID(entityName); ctx_aut->pushContextEntity(entity_id); } diff --git a/rs.hh b/rs.hh index a253a59..3470b70 100644 --- a/rs.hh +++ b/rs.hh @@ -71,6 +71,7 @@ class RctSys void ctxAutEnable(void); void ctxAutAddState(std::string stateName); + void ctxAutSetInitState(std::string stateName); void ctxAutAddTransition(std::string srcStateName, std::string dstStateName); void ctxAutPushNamedContextEntity(std::string entity_name); diff --git a/rsin_parser.ll b/rsin_parser.ll index 8f72e39..ba2cbf8 100644 --- a/rsin_parser.ll +++ b/rsin_parser.ll @@ -47,6 +47,7 @@ blank [ \t] "context-automaton" return token::CONTEXTAUTOMATON; "transitions" return token::TRANSITIONS; "states" return token::STATES; +"init-state" return token::INITSTATE; "rsctl-property" return token::RSCTLFORM; "{" return token::LCB; "}" return token::RCB; diff --git a/rsin_parser.yy b/rsin_parser.yy index 523dfcc..1038cec 100644 --- a/rsin_parser.yy +++ b/rsin_parser.yy @@ -46,7 +46,7 @@ class rsin_driver; %token OPTIONS USE_CTX_AUT USE_CONCENTRATIONS %token REACTIONS INITIALCONTEXTS CONTEXTENTITIES RSCTLFORM -%token CONTEXTAUTOMATON STATES TRANSITIONS +%token CONTEXTAUTOMATON STATES INITSTATE TRANSITIONS %token LCB RCB LRB RRB LSB RSB LAB RAB COL SEMICOL COMMA RARR %token AND OR XOR IMPLIES NOT %token EX EU EF EG AX AU AF AG E A X U F G EMPTY @@ -191,6 +191,7 @@ actentity: IDENTIFIER { ctxaut: | STATES LCB autstates RCB ctxaut + | INITSTATE LCB autinitstate RCB ctxaut | TRANSITIONS LCB auttransitions RCB ctxaut ; @@ -204,6 +205,12 @@ autstates: autstate | autstate COMMA autstates ; + +autinitstate: IDENTIFIER { + driver.getReactionSystem()->ctxAutSetInitState(*$1); + free($1); + } + ; auttransitions: | auttrans