NuSMV nested state machine

[GoogleCodeExporter]

What steps will reproduce the problem?(FileName is sm.ump)
generate NuSMV;

class A {
  sm {
     s1 {
        e1 -> s2;
        e2 -> s2b;
     }
     s2 {
        e1 -> s1;
        s2a {
          e3 -> s2b;
        }
        s2b {
          e3 -> s2a;
        }
     }
  }
}

What is the expected output? (FileName is sm.smv)

-- This file is generated from sm.ump --

MODULE _A_

  VAR 
    state : { s1 , s2 , s2a , s2b }; 
    event : { e1 , e2 , e3 }; 

MODULE _S2_

  VAR 
    _a : _A_;

  ASSIGN
    init(_a.state) := s2a;   

  TRANS
    (_a.state = s2a) -> (
        _a.event = e3 & next(_a.state) = s2b) &
    (_a.state = s2b) -> (
        _a.event = e3 & next(_a.state) = s2a) &
    (_a.event = e1) -> (next(_a.state) = s1) 

MODULE _Sm_

  VAR 
    _a : _A_;
    _s2 : _S2_;   

  ASSIGN
    init(_a.state) := s1;   

  TRANS
    (_a.state = s1) -> (
        (_a.event = e1 & next(_a.state) = s2)  |
        (_a.event = e2 & next(_a.state) = s2b)  ) &
    (_a.state = s2) -> (
        (_a.event = e1 & next(_a.state) = s1) |
    (_s2._a.state = s2a)    )

MODULE main 

  VAR
    _sm : _Sm_;

-- All states are reachable
CTLSPEC (((EF _sm._a.state = s1 & EF _sm._a.state = s2) & EF _sm._a.state = 
s2a) & EF _sm._a.state = s2b)

What do you see instead?

-- This file is generated from sm.ump --

MODULE Sm

  VAR 
    state : { s1 , s2 , s2a , s2b }; 
    event : { e1 , e2 , e3 };  

  ASSIGN
    init(state) := s1;   

  TRANS
    (state = s1) -> (
        (event = e1 & next(state) = s2)  |
        (event = e2 & next(state) = s2b)  ) &
    (state = s2) -> (
        event = e1 & next(state) = s1)

Please use labels and text to provide additional information.

Original issue reported on code.google.com by opeyemi....@gmail.com on 12 Dec 2014 at 10:03

[GoogleCodeExporter]

Original comment by asopa...@gmail.com on 15 Dec 2014 at 4:36

• Added labels: Type-ProjectUG, Diffic-Med
• Removed labels: Type-Defect, Diffic-Easy

[GoogleCodeExporter]

This can be a project for UCOSP students.
- Generate NuSMV specifications from Umple State Machines.
- Involves purely Code Generation.

Original comment by asopa...@gmail.com on 15 Dec 2014 at 4:39