[REVIEW]: Dionysos.jl: a Modular Platform for Smart Symbolic Control

editorialbot commented 3 months ago

Submitting author: !--author-handle-->@adrienbanse@lucaferranti<!--end-editor-- Reviewers: @schillic, @jmskov Archive: Pending

Status

Status badge code:

HTML: <a href="https://proceedings.juliacon.org/papers/645b14c7e9e951673b26b6d8319d3058"><img src="https://proceedings.juliacon.org/papers/645b14c7e9e951673b26b6d8319d3058/status.svg"></a>
Markdown: [![status](https://proceedings.juliacon.org/papers/645b14c7e9e951673b26b6d8319d3058/status.svg)](https://proceedings.juliacon.org/papers/645b14c7e9e951673b26b6d8319d3058)

Reviewers and authors:

Please avoid lengthy details of difficulties in the review thread. Instead, please create a new issue in the target repository and link to those issues (especially acceptance-blockers) by leaving comments in the review thread below. (For completists: if the target issue tracker is also on GitHub, linking the review thread in the issue or vice versa will create corresponding breadcrumb trails in the link target.)

Reviewer instructions & questions

@schillic & @jmskov, your review will be checklist based. Each of you will have a separate checklist that you should update when carrying out your review. First of all you need to run this command in a separate comment to create the checklist:

@editorialbot generate my checklist

The reviewer guidelines are available here: https://joss.readthedocs.io/en/latest/reviewer_guidelines.html. Any questions/concerns please let @lucaferranti know.

✨ Please start on your review when you are able, and be sure to complete your review in the next six weeks, at the very latest ✨

Checklists

📝 Checklist for @jmskov

📝 Checklist for @schillic

editorialbot commented 3 months ago

Hello humans, I'm @editorialbot, a robot that can help you with some common editorial tasks.

For a list of things I can do to help you, just type:

@editorialbot commands

For example, to regenerate the paper pdf after making changes in the paper source files, type:

@editorialbot generate pdf

editorialbot commented 3 months ago

Software report:

github.com/AlDanial/cloc v 1.90  T=0.20 s (1097.0 files/s, 173101.6 lines/s)
-------------------------------------------------------------------------------
Language                     files          blank        comment           code
-------------------------------------------------------------------------------
Julia                          163           2752           2289          19984
TeX                              9            388            270           3131
XML                              7            167             66           1725
CSV                              2              0              0           1676
Markdown                        17            236              0            700
TOML                             6             11              1            189
YAML                             7              7              5            182
Lisp                             2             16              0             69
Ruby                             1              8              4             45
CSS                              1              0              0              4
-------------------------------------------------------------------------------
SUM:                           215           3585           2635          27705
-------------------------------------------------------------------------------

Commit count by author:

    75  Benoît Legat
    64  guberger
    57  adrienbanse
    39  Julien Calbert
    34  labo-admin
    31  github-actions[bot]
    30  Lucas Egidio
    24  Adrien Banse
    16  vdebauche
    15  CompatHelper Julia
    15  Guillaume Berger
    10  7380Xing
     7  Virginie Debauche
     5  JulienCalbert
     3  MDella92
     2  Zheming Wang
     1  Arnaud Browet
     1  Davide De Lazzari
     1  DeligneS
     1  Mahsa Farjadnia
     1  SMattenet
     1  Thiago Alves Lima
     1  ThiagoAlvesLima
     1  aaspeel
     1  raphaeljungers
     1  somyasingh711995
     1  vuille5

editorialbot commented 3 months ago

Paper file info:

📄 Wordcount for paper.tex is 5585

🔴 Failed to discover a Statement of need section in paper

editorialbot commented 3 months ago

License info:

✅ License found: MIT License (Valid open source OSI approved license)

editorialbot commented 3 months ago

Reference check summary (note 'MISSING' DOIs are suggestions that need verification):

OK DOIs

- 10.1007/s12532-023-00239-3 is OK
- 10.1016/s0005-1098(98)00178-2 is OK
- 10.48550/ARXIV.2401.04068 is OK
- 10.48550/ARXIV.2401.03555 is OK
- 10.1145/1967701.1967748 is OK
- 10.5281/ZENODO.10460005 is OK
- 10.1109/tac.2013.2295664 is OK
- 10.24433/CO.6327570.V2 is OK
- 10.48550/ARXIV.2403.09556 is OK
- 10.1145/1967701.1967730 is OK

MISSING DOIs

- 10.1109/jproc.2012.2189792 may be a valid DOI for title: Cyber–physical systems: A perspective at the cente...
- No DOI given, and none found for title: Principles of cyber-physical systems
- No DOI given, and none found for title: Introduction to embedded systems: A cyber-physical...
- No DOI given, and none found for title: Principles of model checking
- No DOI given, and none found for title: Verification and control of hybrid systems: a symb...
- 10.1007/bfb0055622 may be a valid DOI for title: Alternating refinement relations
- No DOI given, and none found for title: Feedback refinement relations for the synthesis of...
- No DOI given, and none found for title: Formal methods for discrete-time dynamical systems
- No DOI given, and none found for title: Model checking of safety properties
- 10.1109/9.989067 may be a valid DOI for title: A Lyapunov approach to incremental stability prope...
- 10.1016/s0005-1098(98)00019-3 may be a valid DOI for title: On contraction analysis for non-linear systems
- 10.1109/cdc.2011.6160424 may be a valid DOI for title: Safety controller synthesis for switched systems u...
- 10.1145/3178126.3178143 may be a valid DOI for title: Multi-layered abstraction-based controller synthes...
- No DOI given, and none found for title: Safety controller synthesis for incrementally stab...
- 10.1007/978-3-642-00602-9_25 may be a valid DOI for title: Discrete-state abstractions of nonlinear systems u...
- 10.1007/978-3-642-14295-6_49 may be a valid DOI for title: Pessoa: A tool for embedded controller synthesis
- No DOI given, and none found for title: SCOTS: A tool for the synthesis of symbolic contro...
- No DOI given, and none found for title: Design of symbolic controllers for networked contr...
- 10.1007/978-3-540-78929-1_15 may be a valid DOI for title: Approximately bisimilar symbolic models for increm...
- No DOI given, and none found for title: CoSyMA: a tool for controller synthesis using mult...
- 10.1145/136035.136043 may be a valid DOI for title: Symbolic boolean manipulation with ordered binary-...
- 10.1016/j.automatica.2005.08.007 may be a valid DOI for title: Barrier certificates for nonlinear model validatio...
- 10.1007/978-3-540-24743-2_32 may be a valid DOI for title: Safety verification of hybrid systems using barrie...
- 10.1109/cdc45484.2021.9683448 may be a valid DOI for title: Alternating simulation on hierarchical abstraction...
- No DOI given, and none found for title: Abstraction-based branch and bound approach to Q-l...
- 10.1109/cdc51059.2022.9992495 may be a valid DOI for title: State-feedback abstractions for optimal control of...
- No DOI given, and none found for title: Data-driven memory-dependent abstractions of dynam...
- 10.23919/acc55779.2023.10156175 may be a valid DOI for title: Data-driven heuristic symbolic models and applicat...
- 10.1109/lcsys.2024.3409106 may be a valid DOI for title: Smart abstraction based on iterative cover and non...
- No DOI given, and none found for title: Reachability analysis and its application to the s...
- No DOI given, and none found for title: JuliaReach: a toolbox for set-based reachability
- 10.1137/141000671 may be a valid DOI for title: Julia: A fresh approach to numerical computing
- 10.1287/ijoc.2021.1067 may be a valid DOI for title: MathOptInterface: a data structure for mathematica...

INVALID DOIs

- None

editorialbot commented 3 months ago

:point_right::page_facing_up: Download article proof :page_facing_up: View article proof on GitHub :page_facing_up: :point_left:

lucaferranti commented 3 months ago

Thank you @adrienbanse for the submission and @schillic and @jmskov for volunteering as reviewers. I will be the editor for this submission.

Reviewers, as first, you can generate your checklist with

@editorialbot generate my checklist

After that, feel free to leave your review comments either here or as issues in the submission repository. You can find more information in the review guide and feel free to ping me at any time if you have questions.

jmskov commented 3 months ago

Review checklist for @jmskov

Conflict of interest

[X] I confirm that I have read the JuliaCon conflict of interest policy and that: I have no COIs with reviewing this work or that any perceived COIs have been waived by JCon for the purpose of this review.

Code of Conduct

[X] I confirm that I read and will adhere to the JuliaCon code of conduct.

General checks

[X] Repository: Is the source code for this software available at the https://github.com/dionysos-dev/Dionysos.jl?
[X] License: Does the repository contain a plain-text LICENSE or COPYING file with the contents of an OSI approved software license?
[X] Contribution and authorship: Has the submitting author (@adrienbanse) made major contributions to the software? Does the full list of paper authors seem appropriate and complete?

Functionality

[X] Installation: Does installation proceed as outlined in the documentation?
[X] Functionality: Have the functional claims of the software been confirmed?
[ ] Performance: If there are any performance claims of the software, have they been confirmed? (If there are no claims, please check off this item.)

Documentation

[X] A statement of need: Do the authors clearly state what problems the software is designed to solve and who the target audience is?
[X] Installation instructions: Is there a clearly-stated list of dependencies? Ideally these should be handled with an automated package management solution.
[X] Example usage: Do the authors include examples of how to use the software (ideally to solve real-world analysis problems).
[X] Functionality documentation: Is the core functionality of the software documented to a satisfactory level (e.g., API method documentation)?
[X] Automated tests: Are there automated tests or manual steps described so that the functionality of the software can be verified?
[ ] Community guidelines: Are there clear guidelines for third parties wishing to 1) Contribute to the software 2) Report issues or problems with the software 3) Seek support

Paper format

[X] Authors: Does the paper.tex file include a list of authors with their affiliations?
[ ] A statement of need: Does the paper have a section titled 'Statement of need' that clearly states what problems the software is designed to solve, who the target audience is, and its relation to other work?
[X] References: Do all archival references that should have a DOI list one (e.g., papers, datasets, software)?

Content

[X] Context: is the scientific context motivating the work correctly presented?
[X] Methodology: is the approach taken in the work justified, presented with enough details and reference to reproduce it?
[X] Results: are the results presented and compared to approaches with similar goals?

adrienbanse commented 3 months ago

@editorialbot commands

editorialbot commented 3 months ago

Hello @adrienbanse, here are the things you can ask me to do:


# List all available commands
@editorialbot commands

# Get a list of all editors's GitHub handles
@editorialbot list editors

# Adds a checklist for the reviewer using this command
@editorialbot generate my checklist

# Set a value for branch
@editorialbot set juliacon-paper as branch

# Run checks and provide information on the repository and the paper file
@editorialbot check repository

# Check the references of the paper for missing DOIs
@editorialbot check references

# Generates the pdf paper
@editorialbot generate pdf

# Generates a LaTeX preprint file
@editorialbot generate preprint

# Get a link to the complete list of reviewers
@editorialbot list reviewers

adrienbanse commented 3 months ago

@editorialbot check references

editorialbot commented 3 months ago

Reference check summary (note 'MISSING' DOIs are suggestions that need verification):

OK DOIs

- 10.1109/JPROC.2012.2189792 is OK
- 10.1017/9781107588981 is OK
- 10.1145/1719010.1719011 is OK
- 10.1007/978-1-4419-0224-5 is OK
- 10.1007/BFb0055622 is OK
- 10.1109/CDC.2014.7039364 is OK
- 10.1007/978-3-319-50763-7 is OK
- 10.1023/A:1011254632723 is OK
- 10.1109/9.989067 is OK
- 10.1109/CDC.2011.6160424 is OK
- 10.1145/3178126.3178143 is OK
- 10.1109/TAC.2015.2478131 is OK
- 10.1145/2883817.2883834 is OK
- 10.1109/TAC.2018.2833630 is OK
- 10.1109/TAC.2009.2034922 is OK
- 10.1145/2461328.2461343 is OK
- 10.1145/136035.136043 is OK
- 10.1016/j.automatica.2005.08.007 is OK
- 10.1109/CDC45484.2021.9683448 is OK
- 10.48550/arXiv.2011.11029 is OK
- 10.1109/CDC51059.2022.9992495 is OK
- 10.48550/arXiv.2212.01926 is OK
- 10.23919/ACC55779.2023.10156175 is OK
- 10.48550/arXiv.2403.02190 is OK
- 10.1145/3302504.3311804 is OK
- 10.1137/141000671 is OK
- 10.1007/s12532-023-00239-3 is OK
- 10.1287/ijoc.2021.1067 is OK
- 10.1016/s0005-1098(98)00178-2 is OK
- 10.48550/ARXIV.2401.04068 is OK
- 10.48550/ARXIV.2401.03555 is OK
- 10.1145/1967701.1967748 is OK
- 10.5281/ZENODO.10460005 is OK
- 10.1109/tac.2013.2295664 is OK
- 10.24433/CO.6327570.V2 is OK
- 10.48550/ARXIV.2403.09556 is OK
- 10.1145/1967701.1967730 is OK

MISSING DOIs

- No DOI given, and none found for title: Reachability analysis and its application to the s...

INVALID DOIs

- 10.5555/1373322 is INVALID
- https://doi.org/10.1016/S0005-1098(98)00019-3 is INVALID because of 'https://doi.org/' prefix
- 10.1007/978-3-642-00602-9\_25 URL is INVALID
- 10.1007/978-3-642-14295-6\_49 URL is INVALID
- 10.1007/978-3-540-24743-2\_32 URL is INVALID

adrienbanse commented 3 months ago

@editorialbot check references

editorialbot commented 3 months ago

Reference check summary (note 'MISSING' DOIs are suggestions that need verification):

OK DOIs

- 10.1109/JPROC.2012.2189792 is OK
- 10.1017/9781107588981 is OK
- 10.1145/1719010.1719011 is OK
- 10.1007/978-1-4419-0224-5 is OK
- 10.1007/BFb0055622 is OK
- 10.1109/CDC.2014.7039364 is OK
- 10.1007/978-3-319-50763-7 is OK
- 10.1023/A:1011254632723 is OK
- 10.1109/9.989067 is OK
- 10.1016/S0005-1098(98)00019-3 is OK
- 10.1109/CDC.2011.6160424 is OK
- 10.1145/3178126.3178143 is OK
- 10.1109/TAC.2015.2478131 is OK
- 10.1145/2883817.2883834 is OK
- 10.1109/TAC.2018.2833630 is OK
- 10.1109/TAC.2009.2034922 is OK
- 10.1145/2461328.2461343 is OK
- 10.1145/136035.136043 is OK
- 10.1016/j.automatica.2005.08.007 is OK
- 10.1109/CDC45484.2021.9683448 is OK
- 10.48550/arXiv.2011.11029 is OK
- 10.1109/CDC51059.2022.9992495 is OK
- 10.48550/arXiv.2212.01926 is OK
- 10.23919/ACC55779.2023.10156175 is OK
- 10.48550/arXiv.2403.02190 is OK
- 10.1145/3302504.3311804 is OK
- 10.1137/141000671 is OK
- 10.1007/s12532-023-00239-3 is OK
- 10.1287/ijoc.2021.1067 is OK
- 10.1016/s0005-1098(98)00178-2 is OK
- 10.48550/ARXIV.2401.04068 is OK
- 10.48550/ARXIV.2401.03555 is OK
- 10.1145/1967701.1967748 is OK
- 10.5281/ZENODO.10460005 is OK
- 10.1109/tac.2013.2295664 is OK
- 10.24433/CO.6327570.V2 is OK
- 10.48550/ARXIV.2403.09556 is OK
- 10.1145/1967701.1967730 is OK

MISSING DOIs

- No DOI given, and none found for title: Principles of model checking
- No DOI given, and none found for title: Reachability analysis and its application to the s...

INVALID DOIs

- 10.1007/978-3-642-00602-9\_25 URL is INVALID
- 10.1007/978-3-642-14295-6\_49 URL is INVALID
- 10.1007/978-3-540-24743-2\_32 URL is INVALID

adrienbanse commented 3 months ago

Thanks a lot for your work @lucaferranti ! Can't do much better for the DOIs

schillic commented 3 months ago

@adrienbanse: The problem is the {\_} in the doi entries. Try _ or, if that does not work, \_.

lucaferranti commented 3 months ago

@adrienbanse RE: DOI

For the missing ones, if the references don't have a DOI, then it's ok
The invalid ones should be fixed, that is generally due to some latex formatting quirkiness and it generally has to do with some underscores, so I think Christian's suggestion is on the money

adrienbanse commented 3 months ago

@editorialbot check references

editorialbot commented 3 months ago

Reference check summary (note 'MISSING' DOIs are suggestions that need verification):

OK DOIs

- 10.1109/JPROC.2012.2189792 is OK
- 10.1017/9781107588981 is OK
- 10.1145/1719010.1719011 is OK
- 10.1007/978-1-4419-0224-5 is OK
- 10.1007/BFb0055622 is OK
- 10.1109/CDC.2014.7039364 is OK
- 10.1007/978-3-319-50763-7 is OK
- 10.1023/A:1011254632723 is OK
- 10.1109/9.989067 is OK
- 10.1016/S0005-1098(98)00019-3 is OK
- 10.1109/CDC.2011.6160424 is OK
- 10.1145/3178126.3178143 is OK
- 10.1109/TAC.2015.2478131 is OK
- 10.1145/2883817.2883834 is OK
- 10.1109/TAC.2018.2833630 is OK
- 10.1109/TAC.2009.2034922 is OK
- 10.1145/2461328.2461343 is OK
- 10.1145/136035.136043 is OK
- 10.1016/j.automatica.2005.08.007 is OK
- 10.1109/CDC45484.2021.9683448 is OK
- 10.48550/arXiv.2011.11029 is OK
- 10.1109/CDC51059.2022.9992495 is OK
- 10.48550/arXiv.2212.01926 is OK
- 10.23919/ACC55779.2023.10156175 is OK
- 10.48550/arXiv.2403.02190 is OK
- 10.1145/3302504.3311804 is OK
- 10.1137/141000671 is OK
- 10.1007/s12532-023-00239-3 is OK
- 10.1287/ijoc.2021.1067 is OK
- 10.1016/s0005-1098(98)00178-2 is OK
- 10.48550/ARXIV.2401.04068 is OK
- 10.48550/ARXIV.2401.03555 is OK
- 10.1145/1967701.1967748 is OK
- 10.5281/ZENODO.10460005 is OK
- 10.1109/tac.2013.2295664 is OK
- 10.24433/CO.6327570.V2 is OK
- 10.48550/ARXIV.2403.09556 is OK
- 10.1145/1967701.1967730 is OK

MISSING DOIs

- No DOI given, and none found for title: Principles of model checking
- No DOI given, and none found for title: Reachability analysis and its application to the s...

INVALID DOIs

- 10.1007/978-3-642-00602-9\_25 URL is INVALID
- 10.1007/978-3-642-14295-6\_49 URL is INVALID
- 10.1007/978-3-540-24743-2\_32 URL is INVALID

adrienbanse commented 3 months ago

@schillic @lucaferranti Thanks for your help. 😃 It seems like all three options (_, \_, {\_}) don't work. Should I just remove the part after the underscore? The DOI would then refer to the proceedings of the whole conference, and not the specific paper (chapter) anymore.

blegat commented 3 months ago

Maybe you can try this https://github.com/JuliaPolyhedra/Polyhedra.jl/blob/06720f03519faef569c92a6d6364fa5a393a9176/paper/paper.tex#L6-L7 Using the underscore package allows you to use the DOI without having to escape the underscores

adrienbanse commented 3 months ago

@editorialbot check references

editorialbot commented 3 months ago

Reference check summary (note 'MISSING' DOIs are suggestions that need verification):

OK DOIs

- 10.1109/JPROC.2012.2189792 is OK
- 10.1017/9781107588981 is OK
- 10.1145/1719010.1719011 is OK
- 10.1007/978-1-4419-0224-5 is OK
- 10.1007/BFb0055622 is OK
- 10.1109/CDC.2014.7039364 is OK
- 10.1007/978-3-319-50763-7 is OK
- 10.1023/A:1011254632723 is OK
- 10.1109/9.989067 is OK
- 10.1016/S0005-1098(98)00019-3 is OK
- 10.1109/CDC.2011.6160424 is OK
- 10.1145/3178126.3178143 is OK
- 10.1109/TAC.2015.2478131 is OK
- 10.1145/2883817.2883834 is OK
- 10.1109/TAC.2018.2833630 is OK
- 10.1109/TAC.2009.2034922 is OK
- 10.1145/2461328.2461343 is OK
- 10.1145/136035.136043 is OK
- 10.1016/j.automatica.2005.08.007 is OK
- 10.1109/CDC45484.2021.9683448 is OK
- 10.48550/arXiv.2011.11029 is OK
- 10.1109/CDC51059.2022.9992495 is OK
- 10.48550/arXiv.2212.01926 is OK
- 10.23919/ACC55779.2023.10156175 is OK
- 10.48550/arXiv.2403.02190 is OK
- 10.1145/3302504.3311804 is OK
- 10.1137/141000671 is OK
- 10.1007/s12532-023-00239-3 is OK
- 10.1287/ijoc.2021.1067 is OK
- 10.1016/s0005-1098(98)00178-2 is OK
- 10.48550/ARXIV.2401.04068 is OK
- 10.48550/ARXIV.2401.03555 is OK
- 10.1145/1967701.1967748 is OK
- 10.5281/ZENODO.10460005 is OK
- 10.1109/tac.2013.2295664 is OK
- 10.24433/CO.6327570.V2 is OK
- 10.48550/ARXIV.2403.09556 is OK
- 10.1145/1967701.1967730 is OK

MISSING DOIs

- No DOI given, and none found for title: Principles of model checking
- No DOI given, and none found for title: Reachability analysis and its application to the s...

INVALID DOIs

- 10.1007/978-3-642-00602-9\textunderscore25 URL is INVALID
- 10.1007/978-3-642-14295-6\textunderscore49 URL is INVALID
- 10.1007/978-3-540-24743-2\textunderscore32 URL is INVALID

adrienbanse commented 3 months ago

@blegat In our paper, the underscore package breaks all the equations using subscripts, also just tried with \textunderscore and it's not allowed by the editorial manager either I'll check for similar issues in previous reviews

schillic commented 3 months ago

@adrienbanse I just checked two old papers of mine and there \_ used to work. I do not know what changed here.

lucaferranti commented 3 months ago

maybe something changed when upgrading from whedon to editorialbot? I can check on how our references process differs from JOSS and see if I spot something

adrienbanse commented 3 months ago

@schillic @lucaferranti The last Whedon code I found (but archived) just appends the string written in the bib file to https://doi.org/ and queries the url, hence the error if it's anything but an underscore

See https://github.com/openjournals/whedon-api/blob/ad17771bc842c1e29fdddc4978c242dbc979454f/workers.rb#L289

  def invalid_doi?(doi_string)
    return true if doi_string.nil?

    if doi_string.include?('http')
      return true
    else
      url = "https://doi.org/#{doi_string}"
    end

    escaped_url = URI.escape(url)

    begin
      status_code = Faraday.head(escaped_url).status
      if [301, 302].include? status_code
        return false
      else
        return true
      end
    rescue Faraday::ConnectionFailed
      return true
    rescue URI::InvalidURIError
      return true
    end
  end

blegat commented 3 months ago

@editorialbot check references

editorialbot commented 3 months ago

Reference check summary (note 'MISSING' DOIs are suggestions that need verification):

OK DOIs

- 10.1109/JPROC.2012.2189792 is OK
- 10.1017/9781107588981 is OK
- 10.1145/1719010.1719011 is OK
- 10.1007/978-1-4419-0224-5 is OK
- 10.1007/BFb0055622 is OK
- 10.1109/CDC.2014.7039364 is OK
- 10.1007/978-3-319-50763-7 is OK
- 10.1023/A:1011254632723 is OK
- 10.1109/9.989067 is OK
- 10.1016/S0005-1098(98)00019-3 is OK
- 10.1109/CDC.2011.6160424 is OK
- 10.1145/3178126.3178143 is OK
- 10.1109/TAC.2015.2478131 is OK
- 10.1007/978-3-642-00602-9_25 is OK
- 10.1007/978-3-642-14295-6_49 is OK
- 10.1145/2883817.2883834 is OK
- 10.1109/TAC.2018.2833630 is OK
- 10.1109/TAC.2009.2034922 is OK
- 10.1145/2461328.2461343 is OK
- 10.1145/136035.136043 is OK
- 10.1016/j.automatica.2005.08.007 is OK
- 10.1007/978-3-540-24743-2_32 is OK
- 10.1109/CDC45484.2021.9683448 is OK
- 10.48550/arXiv.2011.11029 is OK
- 10.1109/CDC51059.2022.9992495 is OK
- 10.48550/arXiv.2212.01926 is OK
- 10.23919/ACC55779.2023.10156175 is OK
- 10.48550/arXiv.2403.02190 is OK
- 10.1145/3302504.3311804 is OK
- 10.1137/141000671 is OK
- 10.1007/s12532-023-00239-3 is OK
- 10.1287/ijoc.2021.1067 is OK
- 10.1016/s0005-1098(98)00178-2 is OK
- 10.48550/ARXIV.2401.04068 is OK
- 10.48550/ARXIV.2401.03555 is OK
- 10.1145/1967701.1967748 is OK
- 10.5281/ZENODO.10460005 is OK
- 10.1109/tac.2013.2295664 is OK
- 10.24433/CO.6327570.V2 is OK
- 10.48550/ARXIV.2403.09556 is OK
- 10.1145/1967701.1967730 is OK

MISSING DOIs

- No DOI given, and none found for title: Principles of model checking
- No DOI given, and none found for title: Reachability analysis and its application to the s...

INVALID DOIs

- None

blegat commented 3 months ago

@editorialbot generate pdf

editorialbot commented 3 months ago

:point_right::page_facing_up: Download article proof :page_facing_up: View article proof on GitHub :page_facing_up: :point_left:

jmskov commented 2 months ago

The package itself looks very useful, and the examples in the paper are compelling. I have some ideas for incorporating probabilistic and unbounded disturbance sets, but that is for another time.

Currently, a couple of tests fail for me on MacOS on fresh Julia 1.6 and 1.10 in different ways. On 1.6, lines 213 and 214 of test_ellipsoids_abstraction.jl fail the approximation check, with Expression: ≈(cost_bound, 0.6250139513432214, rtol = 0.001). A MacOS+RNG issue? On 1.10, there is a conflict with radius with LazySets.jl. Perhaps a version issue.
Running benchmark.jl, I get an undefined SCOTSAbstraction, which I can't seem to find in the relevant module.
(I will update the above comments if I am able to resolve)
No explicit "Statement of need" section in the paper
For the problem definition, time::T, is the number of allowed steps. Can it handle a duration input that determines the maximum number of discrete steps?
Perhaps outside the scope of this package, but adding the capability to return a cost or another measure (probability eh?) with the controller would be useful for the future

blegat commented 2 months ago

Thanks for the review! About the issue with radius, it is fixed by https://github.com/JuliaIntervals/IntervalLinearAlgebra.jl/pull/135. At the moment, you need to checkout this branch of IntervalLinearAlgebra

schillic commented 2 months ago

Review checklist for @schillic

Conflict of interest

[x] I confirm that I have read the JuliaCon conflict of interest policy and that: I have no COIs with reviewing this work or that any perceived COIs have been waived by JCon for the purpose of this review.

Code of Conduct

[x] I confirm that I read and will adhere to the JuliaCon code of conduct.

General checks

[x] Repository: Is the source code for this software available at the https://github.com/dionysos-dev/Dionysos.jl?
[x] License: Does the repository contain a plain-text LICENSE or COPYING file with the contents of an OSI approved software license?
[x] Contribution and authorship: Has the submitting author (@adrienbanse) made major contributions to the software? Does the full list of paper authors seem appropriate and complete?

Functionality

[x] Installation: Does installation proceed as outlined in the documentation?
[x] Functionality: Have the functional claims of the software been confirmed?
[x] Performance: If there are any performance claims of the software, have they been confirmed? (If there are no claims, please check off this item.)

Documentation

[x] A statement of need: Do the authors clearly state what problems the software is designed to solve and who the target audience is?
[x] Installation instructions: Is there a clearly-stated list of dependencies? Ideally these should be handled with an automated package management solution.
[x] Example usage: Do the authors include examples of how to use the software (ideally to solve real-world analysis problems).
[x] Functionality documentation: Is the core functionality of the software documented to a satisfactory level (e.g., API method documentation)?
[x] Automated tests: Are there automated tests or manual steps described so that the functionality of the software can be verified?
[x] Community guidelines: Are there clear guidelines for third parties wishing to 1) Contribute to the software 2) Report issues or problems with the software 3) Seek support

Paper format

[x] Authors: Does the paper.tex file include a list of authors with their affiliations?
[x] A statement of need: Does the paper have a section titled 'Statement of need' that clearly states what problems the software is designed to solve, who the target audience is, and its relation to other work?
[x] References: Do all archival references that should have a DOI list one (e.g., papers, datasets, software)?

Content

[x] Context: is the scientific context motivating the work correctly presented?
[x] Methodology: is the approach taken in the work justified, presented with enough details and reference to reproduce it?
[x] Results: are the results presented and compared to approaches with similar goals?

schillic commented 2 months ago

I did not yet try out the library itself (will do that in the near future). I have filled out the checklist (above) and below I have some comments on the paper. There is only one major comment, which I hope you can fix or explain. Overall a really nice paper (and package - from what I can tell so far) :+1:

Summary

The paper introduces Dionysos.jl, a Julia library for controller synthesis based on abstraction. The library has a modular structure, offering systems, problems, algorithms, set representations, etc. Currently, a key feature of Dionysos are methods based on lazy and non-partition abstraction of the state space. The usage is explained with an extensive example, and the capabilities are demonstrated in a comparison to SCOTS and CoSyMA (which is available on CodeOcean - which I think is a great effort!).

Main comment

There is a mismatch between Definition 3, defined over infinite words, and the behavior $B(S)$, which can be finite or infinite. Since specifications require only infinite behavior, but every infinite behavior induces finite prefixes, that makes any behavior violate any specification.

Checklist comments

Installation instructions: The README points to https://julialang.github.io/Pkg.jl/v1/managing-packages/#Adding-unregistered-packages, but the package is registered. This should be updated, probably to https://dionysos-dev.github.io/Dionysos.jl/stable/developers/setup/.
A statement of need: While there is no dedicated section, the purpose of the package is clearly communicated.

Minor comments

p. 1: "solving optimal control problems using state-of-the-art control techniques, from control" - I guess the 2nd "control" could be dropped.
p. 2: "integer numbers" -> just "integers"?
p. 2 last paragraph on the left: Should it be $k$ ∈ { $0, ..., T-1$ }?
It may be better to move Fig. 2 to the next page so that it is closer to the corresponding text.
Fig. 2 and p. 3: I do not see why a strict single-valued map must induce a partition. Could $R_1$ not map all states $a$ to the same state $b$?
Fig. 3: I do not understand where the red box comes from. Consequently, it is unclear to me why the two cells on the right are also red. Is that an overestimate of $F_1$?
Fig. 4: What does $\kappa \in U_2$ mean? $\kappa$ is a function, right?
p. 4: "specified specifications" - a bit convoluted
p. 4: "cost. :"
p. 4: ", it complements" -> "and complements"
Section 4.2 mentions that obstacles are encoded as part of the domain. Maybe it is worth mentioning again that the Domain module is not described in the paper.
p. 5: SafetyProblem: "the set $X_I$" -> "the initial set $X_I$" (for consistency)
p. 6: Consider merging the definition of an ellipsoid (8) with the one at the end of Section 3.
p. 6: "LazyEllispoidsAbstraction" -> "LazyEllipsoidsAbstraction"
Could you expand the explanation of Fig. 7? What does the arrow from the white center of the figure mean? And do I understand correctly that no further abstract states are reachable? Maybe you can also highlight the initial and target sets (in a different color), like in the web tutorial.
p. 7: "Comparaison" -> "Comparison"

schillic commented 2 months ago

I had a look at the code and have some comments:

Already reported, but for completeness

I confirm the failing test (at least one, did not check for more).
WARNING: both LazySets and IntervalArithmetic export "radius"; uses of it in module IntervalLinearAlgebra must be qualified
- This is really a problem because I cannot run the example in the paper without a crash:
ERROR: UndefVarError: radius not defined

Further warnings

WARNING: using LazySets.vertices in module Utils conflicts with an existing identifier.

There are some duplicate method definitions (presumably from a merge conflict) in src/optim/abstraction/:

WARNING: Method definition (::Type{Dionysos.Optim.Abstraction.LazyAbstraction.Optimizer{T} where T})() in module LazyAbstraction at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_abstraction.jl:66 overwritten at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_abstraction.jl:87.
WARNING: Method definition is_empty(Dionysos.Optim.Abstraction.LazyAbstraction.Optimizer{T} where T) in module LazyAbstraction at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_abstraction.jl:68 overwritten at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_abstraction.jl:89.
WARNING: Method definition set(Dionysos.Optim.Abstraction.LazyAbstraction.Optimizer{T} where T, MathOptInterface.RawOptimizerAttribute, Any) in module LazyAbstraction at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_abstraction.jl:70 overwritten at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_abstraction.jl:91.
WARNING: Method definition get(Dionysos.Optim.Abstraction.LazyAbstraction.Optimizer{T} where T, MathOptInterface.RawOptimizerAttribute) in module LazyAbstraction at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_abstraction.jl:83 overwritten at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_abstraction.jl:94.

WARNING: Method definition (::Type{Dionysos.Optim.Abstraction.HierarchicalAbstraction.Optimizer{T} where T})() in module HierarchicalAbstraction at ~/.julia/dev/Dionysos/src/optim/abstraction/hierarchical_abstraction.jl:75 overwritten at ~/.julia/dev/Dionysos/src/optim/abstraction/hierarchical_abstraction.jl:88.
WARNING: Method definition is_empty(Dionysos.Optim.Abstraction.HierarchicalAbstraction.Optimizer{T} where T) in module HierarchicalAbstraction at ~/.julia/dev/Dionysos/src/optim/abstraction/hierarchical_abstraction.jl:77 overwritten at ~/.julia/dev/Dionysos/src/optim/abstraction/hierarchical_abstraction.jl:90.
WARNING: Method definition set(Dionysos.Optim.Abstraction.HierarchicalAbstraction.Optimizer{T} where T, MathOptInterface.RawOptimizerAttribute, Any) in module HierarchicalAbstraction at ~/.julia/dev/Dionysos/src/optim/abstraction/hierarchical_abstraction.jl:79 overwritten at ~/.julia/dev/Dionysos/src/optim/abstraction/hierarchical_abstraction.jl:92.

WARNING: Method definition (::Type{Dionysos.Optim.Abstraction.LazyEllipsoidsAbstraction.Optimizer{T} where T})() in module LazyEllipsoidsAbstraction at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_ellipsoids_abstraction.jl:84 overwritten at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_ellipsoids_abstraction.jl:101.
WARNING: Method definition is_empty(Dionysos.Optim.Abstraction.LazyEllipsoidsAbstraction.Optimizer{T} where T) in module LazyEllipsoidsAbstraction at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_ellipsoids_abstraction.jl:86 overwritten at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_ellipsoids_abstraction.jl:103.
WARNING: Method definition set(Dionysos.Optim.Abstraction.LazyEllipsoidsAbstraction.Optimizer{T} where T, MathOptInterface.RawOptimizerAttribute, Any) in module LazyEllipsoidsAbstraction at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_ellipsoids_abstraction.jl:88 overwritten at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_ellipsoids_abstraction.jl:105.
WARNING: Method definition get(Dionysos.Optim.Abstraction.LazyEllipsoidsAbstraction.Optimizer{T} where T, MathOptInterface.RawOptimizerAttribute) in module LazyEllipsoidsAbstraction at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_ellipsoids_abstraction.jl:97 overwritten at ~/.julia/dev/Dionysos/src/optim/abstraction/lazy_ellipsoids_abstraction.jl:111.

lucaferranti commented 1 month ago

Hi everyone :wave: ,

just checking in on how this is going.

@blegat have you addressed the comments from the reviewer (the issue in IntervalLinearAlgebra.jl should be fixed now)? If yes, feel free to ping them to take a second look? Otherwise, do you have an estimate timeline?

blegat commented 1 month ago

Thanks for the help with IntervalLinearAlgebra. We're still working on addressing the reviews, see https://github.com/dionysos-dev/Dionysos.jl/pull/361.

adrienbanse commented 2 weeks ago

@editorialbot generate pdf

editorialbot commented 2 weeks ago

:point_right::page_facing_up: Download article proof :page_facing_up: View article proof on GitHub :page_facing_up: :point_left:

adrienbanse commented 2 weeks ago

Many thanks @jmskov and @schillic for the time you spent reviewing this paper, thanks @lucaferranti for your work as editor and thank you all for your patience. 😄

We normally addressed all the unclarities/questions from your reviews. All the changes in the paper are written in red.

@jmskov

Currently, a couple of tests fail for me on MacOS on fresh Julia 1.6 and 1.10 in different ways. On 1.6, lines 213 and 214 of test_ellipsoids_abstraction.jl fail the approximation check, with Expression: ≈(cost_bound, 0.6250139513432214, rtol = 0.001). A MacOS+RNG issue? On 1.10, there is a conflict with radius with LazySets.jl. Perhaps a version issue.

Running benchmark.jl, I get an undefined SCOTSAbstraction, which I can't seem to find in the relevant module.

Thanks for reporting this! The two problems are normally solved in the latest version of Dionysos. Note that we bumped the Julia version of Dionysos to 1.10, as it will soon become the new LTS (as soon as 1.11 is out).

No explicit "Statement of need" section in the paper

We understood from previous reviews that "the consensus was that as long as the statement of need is clearly conveyed in the paper, it's not needed to have a section verbatim with that name" (citing @lucaferranti). Please let us know if you think that it would be better with an explicit "Statement of need" section.

For the problem definition, time::T, is the number of allowed steps. Can it handle a duration input that determines the maximum number of discrete steps?

If I understood well, yes! This parameter can typically be used like this.

Perhaps outside the scope of this package, but adding the capability to return a cost or another measure (probability eh?) with the controller would be useful for the future

Thanks for proposing new features! In the current state of Dionysos, in some situations, this cost can be computed a posteriori. We modified the caption of Figure 6 to include an example of computation of such a bound on the cost.

@schillic

There is a mismatch between Definition 3, defined over infinite words, and the behavior B(S) , which can be finite or infinite. Since specifications require only infinite behavior, but every infinite behavior induces finite prefixes, that makes any behavior violate any specification.

Thanks for reporting this problem. We modified Definition 3 so that both finite and infinite time specifications are handled.

Minor comments

Thanks for reporting the unclarities and typos written in this section! We agree with all of the remarks, and we modified the paper accordingly to all of them. We answer to the following remark:

Fig. 2 and p. 3: I do not see why a strict single-valued map must induce a partition. Could R1 not map all states a to the same state b?

A partition is defined as a collection of sets that 1) covers the state space and 2) don't intersect with each other. A function (that is, a single-valued map) maps every point of the state space (making it a covering) to a unique symbol (making it non-intersecting with each other), and thereby automatically defines a partition. The case where R1 maps all states to the same state b corresponds to a trivial partition with only one bloc.

Already reported, but for completeness

All problems reported in this section are normally solved in the latest version of Dionysos (see answer above).

Further warnings

WARNING: using LazySets.vertices in module Utils conflicts with an existing identifier.

There are some duplicate method definitions (presumably from a merge conflict) in src/optim/abstraction/:

Thanks for spotting these two errors! Again, normally this has been solved in the latest version of Dionysos.

lucaferranti commented 2 weeks ago

We understood from previous reviews that "the consensus was that as long as the statement of need is clearly conveyed in the paper, it's not needed to have a section verbatim with that name" (citing @lucaferranti). Please let us know if you think that it would be better with an explicit "Statement of need" section

correct! The work should of course be clearly motivated in the paper, but a section called statement of need is not needed. This was the most frequently asked question and we recently clarified that in the review checklist (unfortunately already generated checklists are not modififed). The new wording is:

Does the paper clearly explain the problem it addresses, its importance to the broader community, the intended audience, and how it connects to existing work in the field?

JuliaCon / proceedings-review