tree.py 15 KB

123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410
  1. import termcolor
  2. from typing import *
  3. import itertools
  4. from sccd.statechart.static.action import *
  5. from sccd.statechart.static.state_ref import StateRef
  6. from sccd.util.bitmap import *
  7. from sccd.util import timer
  8. from sccd.util.visit_tree import *
  9. from sccd.util.freezable import *
  10. from abc import *
  11. @dataclass(eq=False)
  12. class AbstractState:
  13. short_name: str # value of 'id' attribute in XML
  14. parent: Optional['AbstractState'] # only None if root state
  15. children: List['AbstractState'] = field(default_factory=list)
  16. ####### Calculated values below ########
  17. state_id: int = -1
  18. state_id_bitmap: Bitmap = Bitmap() # bitmap with only state_id-bit set
  19. full_name: str = ""
  20. ancestors: Bitmap = Bitmap()
  21. descendants: Bitmap = Bitmap()
  22. effective_targets: Bitmap = Bitmap()
  23. def __post_init__(self):
  24. if self.parent is not None:
  25. self.parent.children.append(self)
  26. def __str__(self):
  27. return "AbstractState(%s)" % self.short_name
  28. __repr__ = __str__
  29. @dataclass(eq=False)
  30. class State(AbstractState, Visitable):
  31. type: 'StateType' = None
  32. real_children: List['State'] = field(default_factory=list) # children, but not including pseudo-states such as history
  33. # whether this is a stable stabe. this field is ignored if maximality semantics is not set to SYNTACTIC
  34. stable: bool = False
  35. # Outgoing transitions
  36. transitions: List['Transition'] = field(default_factory=list)
  37. enter: List[Action] = field(default_factory=list)
  38. exit: List[Action] = field(default_factory=list)
  39. ####### Calculated values below ########
  40. depth: int = -1 # Root is 0, root's children are 1, and so on
  41. # If a direct child of this state is a deep history state, then "deep history" needs to be recorded when exiting this state. This value contains a tuple, with the (history-id, history_mask, history state) of that child state.
  42. deep_history: Optional[Tuple[int, Bitmap, 'DeepHistoryState']] = None
  43. # If a direct child of this state is a shallow history state, then "shallow history" needs to be recorded when exiting this state. This value is the history-id of that child state
  44. shallow_history: Optional[Tuple[int, 'ShallowHistoryState']] = None
  45. # Triggers of outgoing transitions that are AfterTrigger.
  46. after_triggers: List['AfterTrigger'] = field(default_factory=list)
  47. def __post_init__(self):
  48. super().__post_init__()
  49. if self.parent is not None:
  50. self.parent.real_children.append(self)
  51. def __str__(self):
  52. if isinstance(self.type, AndState):
  53. return "AndState(%s)" % self.short_name
  54. elif isinstance(self.type, OrState):
  55. return "OrState(%s)" % self.short_name
  56. else:
  57. return "State?(%s)" % self.short_name
  58. __repr__ = __str__
  59. @dataclass(eq=False)
  60. class HistoryState(AbstractState):
  61. history_id: int = -1
  62. def __post_init__(self):
  63. super().__post_init__()
  64. self.type = HistoryStateType(self)
  65. @dataclass(eq=False)
  66. class ShallowHistoryState(HistoryState):
  67. def __str__(self):
  68. return "ShallowHistoryState(%s)" % self.short_name
  69. __repr__ = __str__
  70. @dataclass(eq=False)
  71. class DeepHistoryState(HistoryState):
  72. def __str__(self):
  73. return "DeepHistoryState(%s)" % self.short_name
  74. __repr__ = __str__
  75. @dataclass(eq=False)
  76. class StateType(ABC):
  77. state: State
  78. @abstractmethod
  79. def effective_targets(self):
  80. pass
  81. @abstractmethod
  82. def additional_effective_targets(self, exclude: 'State'):
  83. pass
  84. @dataclass(eq=False)
  85. class AndState(StateType):
  86. def effective_targets(self):
  87. return self.additional_effective_targets(None)
  88. def additional_effective_targets(self, exclude: 'State'):
  89. return [self.state] + list(itertools.chain(*(c.type.effective_targets() for c in self.state.children if not isinstance(c, HistoryState) and c is not exclude)))
  90. @dataclass(eq=False)
  91. class OrState(StateType):
  92. default_state: AbstractState
  93. def effective_targets(self):
  94. return [self.state] + self.default_state.type.effective_targets()
  95. def additional_effective_targets(self, exclude: 'State'):
  96. return [self.state]
  97. @dataclass(eq=False)
  98. class HistoryStateType(StateType):
  99. def effective_targets(self):
  100. return []
  101. def additional_effective_targets(self, exclude: 'State'):
  102. assert False # history state cannot have children and therefore should never occur in a "enter path"
  103. @dataclass
  104. class EventDecl:
  105. __slots__ = ["name", "params_decl"]
  106. name: str
  107. params_decl: List[ParamDecl]
  108. def render(self) -> str:
  109. if self.params_decl:
  110. return self.name + '(' + ', '.join(p.render() for p in self.params_decl) + ')'
  111. else:
  112. return self.name
  113. @dataclass
  114. class Trigger:
  115. __slots__ = ["enabling", "enabling_bitmap"]
  116. enabling: List[EventDecl]
  117. def check(self, events: List[InternalEvent]) -> bool:
  118. for e in self.enabling:
  119. if e.name not in (e.name for e in events):
  120. return False
  121. return True
  122. def render(self) -> str:
  123. return ' ∧ '.join(e.render() for e in self.enabling)
  124. @dataclass
  125. class NegatedTrigger(Trigger):
  126. __slots__ = ["disabling", "disabling_bitmap"]
  127. disabling: List[EventDecl]
  128. def check(self, events: List[InternalEvent]) -> bool:
  129. if not Trigger.check(self, events):
  130. return False
  131. for e in self.disabling:
  132. if e.name in (e.name for e in events):
  133. return False
  134. return True
  135. def render(self) -> str:
  136. return ' ∧ '.join(itertools.chain((e.render() for e in self.enabling), ('¬'+e.render() for e in self.disabling)))
  137. class AfterTrigger(Trigger):
  138. def __init__(self, name: str, after_id: int, delay: Expression):
  139. enabling = [EventDecl(name=name, params_decl=[])]
  140. super().__init__(enabling)
  141. # self.id = id
  142. self.name = name
  143. self.after_id = after_id # unique ID for AfterTrigger
  144. self.delay = delay
  145. def render(self) -> str:
  146. return "after("+self.delay.render()+")"
  147. EMPTY_TRIGGER = Trigger(enabling=[])
  148. @dataclass(eq=False)
  149. class Transition(StateRef):
  150. guard: Optional[FunctionDeclaration] = None
  151. actions: List[Action] = field(default_factory=list)
  152. trigger: Trigger = EMPTY_TRIGGER
  153. ####### CALCULATED VALUES ########
  154. id: int = None # just a unique number, >= 0
  155. exit_mask: State = None
  156. arena: State = None
  157. arena_bitmap: Bitmap = None
  158. # The "enter set" can be computed partially statically, or entirely statically if there are no history states in it.
  159. enter_states_static: Bitmap = None
  160. target_history_id: Optional[int] = None # History ID if target of transition is a history state, otherwise None.
  161. target_stable: bool = None # Whether target state is a stable state
  162. raised_events: Bitmap = None # (internal) event IDs raised by this transition
  163. def __str__(self):
  164. if self.target is None:
  165. return "Transition(%s -> %s)" % (self.source.short_name, self.target_string)
  166. else:
  167. return termcolor.colored("%s -> %s" % (self.source.full_name, self.target.full_name), 'green')
  168. __repr__ = __str__
  169. class StateTree:
  170. def __init__(self, root: State):
  171. super().__init__()
  172. self.root: State = root
  173. self.state_dict = {}
  174. self.state_list = []
  175. self.transition_list = []
  176. self.timer_count = 0 # number of after-transitions in the statechart
  177. self.history_states: List[HistoryState] = []
  178. self.initial_history_values: List[Bitmap] = []
  179. with timer.Context("optimize tree"):
  180. def assign_state_id():
  181. next_id = 0
  182. def f(state: State, _=None):
  183. nonlocal next_id
  184. state.state_id = next_id
  185. state.state_id_bitmap = bit(next_id)
  186. next_id += 1
  187. return f
  188. def assign_full_name(state: State, parent_full_name: str = ""):
  189. if state is root:
  190. full_name = '/'
  191. elif state.parent is root:
  192. full_name = '/' + state.short_name
  193. else:
  194. full_name = parent_full_name + '/' + state.short_name
  195. state.full_name = full_name
  196. return full_name
  197. def assign_depth(state: State, parent_depth: int = 0):
  198. state.depth = parent_depth + 1
  199. return parent_depth + 1
  200. def add_to_list(state: State ,_=None):
  201. self.state_dict[state.full_name] = state
  202. self.state_list.append(state)
  203. def visit_transitions(state: State, _=None):
  204. for t in state.transitions:
  205. self.transition_list.append(t)
  206. if t.trigger and isinstance(t.trigger, AfterTrigger):
  207. state.after_triggers.append(t.trigger)
  208. self.timer_count += 1
  209. def set_ancestors(state: State, ancestors=Bitmap()):
  210. state.ancestors = ancestors
  211. return ancestors | state.state_id_bitmap
  212. def set_descendants(state: State, children_descendants):
  213. descendants = bm_union(children_descendants)
  214. state.descendants = descendants
  215. return state.state_id_bitmap | descendants
  216. def calculate_effective_targets(state: State, _=None):
  217. # implementation of "effective_targets"-method is recursive (slow)
  218. # store the result, it is always the same:
  219. state.effective_targets = states_to_bitmap(state.type.effective_targets())
  220. def deal_with_history(state: State, children_history):
  221. for h in children_history:
  222. if isinstance(h, DeepHistoryState):
  223. state.deep_history = (h.history_id, h.parent.descendants, h)
  224. elif isinstance(h, ShallowHistoryState):
  225. state.shallow_history = (h.history_id, h)
  226. if isinstance(state, HistoryState):
  227. state.history_id = len(self.initial_history_values) # generate history ID
  228. self.history_states.append(state)
  229. self.initial_history_values.append(state.parent.effective_targets)
  230. return state
  231. visit_tree(root, lambda s: s.children,
  232. parent_first=[
  233. assign_state_id(),
  234. assign_full_name,
  235. add_to_list,
  236. set_ancestors,
  237. ],
  238. child_first=[
  239. set_descendants,
  240. calculate_effective_targets,
  241. ])
  242. visit_tree(root, lambda s: s.real_children,
  243. parent_first=[
  244. assign_depth,
  245. visit_transitions,
  246. ],
  247. child_first=[])
  248. self.initial_states = root.effective_targets
  249. visit_tree(root, lambda s: s.children,
  250. child_first=[
  251. deal_with_history,
  252. ])
  253. # print()
  254. # def pretty_print(s, indent=""):
  255. # print(indent, s)
  256. # return indent + " "
  257. # visit_tree(root, lambda s: s.children,
  258. # parent_first=[
  259. # pretty_print,
  260. # ])
  261. for t_id, t in enumerate(self.transition_list):
  262. # Arena can be computed statically. First compute Lowest-common ancestor:
  263. arena = self.lca(t.source, t.target)
  264. # Arena must be an Or-state:
  265. while not isinstance(arena.type, OrState):
  266. arena = arena.parent
  267. # Exit states can be efficiently computed at runtime based on the set of current states.
  268. # Enter states are more complex but luckily, can be computed *partially* statically:
  269. # As a start, we calculate the enter path:
  270. # The enter path is the path from arena to the target state (including the target state, but not including the arena).
  271. # Enter path is the intersection between:
  272. # 1) the transition's target and its ancestors, and
  273. # 2) the arena's descendants
  274. enter_path = (t.target.state_id_bitmap | t.target.ancestors) & arena.descendants
  275. # All states on the enter path will be entered, but on the enter path, there may also be AND-states whose children are not on the enter path, but should also be entered.
  276. enter_path_iter = self.bitmap_to_states(enter_path)
  277. entered_state = next(enter_path_iter, None)
  278. enter_states_static = Bitmap()
  279. while entered_state is not None:
  280. next_entered_state = next(enter_path_iter, None)
  281. if next_entered_state:
  282. # an intermediate state on the path from arena to target
  283. enter_states_static |= states_to_bitmap(entered_state.type.additional_effective_targets(next_entered_state))
  284. else:
  285. # the actual target of the transition
  286. enter_states_static |= entered_state.effective_targets
  287. entered_state = next_entered_state
  288. target_history_id = None
  289. if isinstance(t.target, HistoryState):
  290. target_history_id = t.target.history_id
  291. target_stable = False
  292. if isinstance(t.target, State):
  293. target_stable = t.target.stable
  294. raised_events = []
  295. for a in t.actions:
  296. if isinstance(a, RaiseInternalEvent):
  297. raised_events.append(a.name)
  298. t.id = t_id
  299. t.exit_mask = arena.descendants
  300. t.arena = arena
  301. t.arena_bitmap = arena.descendants | arena.state_id_bitmap
  302. t.enter_states_static = enter_states_static
  303. t.target_history_id = target_history_id
  304. t.target_stable = target_stable
  305. t.raised_events = raised_events
  306. def bitmap_to_states(self, bitmap: Bitmap) -> Iterator[State]:
  307. return (self.state_list[id] for id in bm_items(bitmap))
  308. def bitmap_to_states_reverse(self, bitmap: Bitmap) -> Iterator[State]:
  309. return (self.state_list[id] for id in bm_reverse_items(bitmap))
  310. def lca(self, s1: State, s2: State) -> State:
  311. # Intersection between source & target ancestors, last member in depth-first sorted state list.
  312. return self.state_list[bm_highest_bit((s1.ancestors) & (s2.ancestors))]
  313. def states_to_bitmap(states: Iterable[State]) -> Bitmap:
  314. return bm_from_list(s.state_id for s in states)
  315. # Is parent ancestor of child? Also returns true when parent IS child.
  316. # If this function returns True, and child is a current state, then parent will be too.
  317. def is_ancestor(parent: State, child: State) -> bool:
  318. return bm_has(child.ancestors | child.state_id_bitmap, parent.state_id)