Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Additional state machine for topics handling #64

Open
MarcoLm993 opened this issue Oct 25, 2024 · 0 comments
Open

Additional state machine for topics handling #64

MarcoLm993 opened this issue Oct 25, 2024 · 0 comments
Labels
feature New feature or request priority: middle

Comments

@MarcoLm993
Copy link
Collaborator

MarcoLm993 commented Oct 25, 2024

Mentioned in comment: #63 (comment)

The discussion came up for supporting SCAN's property checking, that requires to know at least the target or the origin of a specific event for checking a property on it. This is an issue when modeling ROS-topic communication, that could have more than one publisher and more than one subscriber on the same topic.
To address the limitation, we want to have an additional state machine that:

  • receives all messages from all publishers
  • sends the same events to the related automata
    While this is definitely required for SCAN, for the Jani conversion it is not completely obvious it makes sense, since it would come with the following strings attached:
  • Each topic consists of 3 additional automata (1 for the topic itself and 2 for communication to and from the topic automaton, compared to the current state where there is only one automaton per topic)
  • Each topic required 3 sets of variables (one for storing the new message (internal, might be also an array) and 2 for communication, currently only one set is required (global)

Needs to be checked out...

@MarcoLm993 MarcoLm993 added feature New feature or request priority: middle labels Oct 25, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
feature New feature or request priority: middle
Projects
None yet
Development

No branches or pull requests

1 participant