Git Product home page Git Product logo

tl-grammars's Introduction

Standard Grammar for Temporal Logics

HTML Manuscript PDF Manuscript GitHub Actions Status

This repository contains a standard grammar for LTL and LDL.

Link to the latest published version paper (on ArXiv): https://arxiv.org/abs/2012.13638

Link to the latest version on GitHub: https://marcofavorito.me/tl-grammars

Manubot

Manubot is a system for writing scholarly manuscripts via GitHub. Manubot automates citations and references, versions manuscripts using git, and enables collaborative writing via GitHub. An overview manuscript presents the benefits of collaborative writing with Manubot and its unique features. The rootstock repository is a general purpose template for creating new Manubot instances, as detailed in SETUP.md. See USAGE.md for documentation how to write a manuscript.

Please open an issue for questions related to Manubot usage, bug reports, or general inquiries.

Repository directories & files

The directories are as follows:

  • content contains the manuscript source, which includes markdown files as well as inputs for citations and references. See USAGE.md for more information.
  • output contains the outputs (generated files) from Manubot including the resulting manuscripts. You should not edit these files manually, because they will get overwritten.
  • webpage is a directory meant to be rendered as a static webpage for viewing the HTML manuscript.
  • build contains commands and tools for building the manuscript.
  • ci contains files necessary for deployment via continuous integration.

In content/grammars/ you can find implementations of the standard. Currently, there's only the implementation in ANTLR4 (in grammars/antlr4/).

Build

We use Manubot to build the document in PDF and HTML formats.

Local execution

The easiest way to run Manubot is to use continuous integration to rebuild the manuscript when the content changes. If you want to build a Manubot manuscript locally, install the conda environment as described in build. Then, you can build the manuscript on POSIX systems by running the following commands from this root directory.

# Activate the manubot conda environment (assumes conda version >= 4.4)
conda activate manubot

# Build the manuscript, saving outputs to the output directory
bash build/build.sh

# At this point, the HTML & PDF outputs will have been created. The remaining
# commands are for serving the webpage to view the HTML manuscript locally.
# This is required to view local images in the HTML output.

# Configure the webpage directory
manubot webpage

# You can now open the manuscript webpage/index.html in a web browser.
# Alternatively, open a local webserver at http://localhost:8000/ with the
# following commands.
cd webpage
python -m http.server

Sometimes it's helpful to monitor the content directory and automatically rebuild the manuscript when a change is detected. The following command, while running, will trigger both the build.sh script and manubot webpage command upon content changes:

bash build/autobuild.sh

Continuous Integration

Whenever a pull request is opened, CI (continuous integration) will test whether the changes break the build process to generate a formatted manuscript. The build process aims to detect common errors, such as invalid citations. If your pull request build fails, see the CI logs for the cause of failure and revise your pull request accordingly.

When a commit to the main branch occurs (for example, when a pull request is merged), CI builds the manuscript and writes the results to the gh-pages and output branches. The gh-pages branch uses GitHub Pages to host the following URLs:

For continuous integration configuration details, see .github/workflows/manubot.yaml if using GitHub Actions or .travis.yml if using Travis CI.

Contribute

To contribute do one of the following:

License

License: CC BY 4.0 License: CC0 1.0

Except when noted otherwise, the entirety of this repository is licensed under a CC BY 4.0 License (LICENSE.md), which allows reuse with attribution. Please attribute by linking to https://github.com/marcofavorito/tl-grammars.

Since CC BY is not ideal for code and data, certain repository components are also released under the CC0 1.0 public domain dedication (LICENSE-CC0.md). All files matched by the following glob patterns are dual licensed under CC BY 4.0 and CC0 1.0:

  • *.sh
  • *.py
  • *.yml / *.yaml
  • *.json
  • *.bib
  • *.tsv
  • .gitignore

All other files are only available under CC BY 4.0, including:

  • *.md
  • *.html
  • *.pdf
  • *.docx

Please open an issue for any question related to licensing.

tl-grammars's People

Contributors

marcofavorito avatar

Stargazers

 avatar  avatar  avatar

Watchers

 avatar  avatar  avatar

tl-grammars's Issues

Make upper-case reserved

Some upper-case characters should be made reserved, as these are used in LTLf and PLTLf. E.g. X, F, G

Explain difference between "propositional not" and "logical not" in LTLf and PLTLf

Currently, in LTLf and PLTLf, there is no enough stress on the difference between the "propositional not" and the "logical not" in front of propositional atoms.

Consider the LTLf syntax in negation normal form:

f := a  |  !a  |  f1 & f2  |  f1|f2  |  X[!](f)  |  X(f)  |  f1 U f2  |  f1 R f2

The formula a accepts the following language: all the non-empty traces that start with a propositional interpretation in which a holds.

Let's denote the propositional negation with ! (can only occur in front of atomic formulas), and the logical negation with ~ .

A logical negation of a, let us write it ~a, results in a language whose traces are: either empty-trace or any trace that starts with a propositional interpretation in which a does not hold.

However, a propositional negation !a differs from ~a by NOT accepting the empty trace.

To give a better idea, here are the automata corresponding to each formula:

  • a:
    image

  • !a:
    image

  • ~a:
    image

  • ~(!a):
    image

Similar reasoning applies to PLTLf.

The purpose of this issue is to keep track of this subtle difference. My opinion is to avoid introducing two different symbols for the negation, ~ and ! in the example above, as it leads to confusion.
We could assume that !f of ~f means "logical not f" if f is NOT an atomic formula, and "propositional not f" if f is an atomic formula; then, to write ~a in the example above (i.e. the logical not in front of atomic formula), one could rely on the equivalence:

~a <-> (!a | end)

Where end is a formula that only accepts the empty trace, e.g. by convention it could be G(false).

Then, the logical negation of !a can be rewritten as:

~(!a) <-> ~(~a & ~end) <-> (a | end)

In summary, I propose to have two equivalent symbols for the negation, i.e. ! and ~ are interchangeable. However, the negation assumes two different meanings depending on what kind of formula is in its argument; if it is an atomic formula, then it is interpreted as a propositional negation, and if not, it is interpreted as a logical negation.
For example, the above three formulas would have been written as: a, !a, !a | end and a | end, respectively.

The implementer of the grammar will take into account these two differences at the code level, and e.g. to transform in NNF it should rely on the above equivalences.

Typo in section "2.1 Characters"

At the point where the supported character ranges are specified:

The range of characters to be supported is defined as:

Char ::= [#x9 | #xA | #xD | [#x20-#x7e]

There is a wrong square bracket just before #x9. It should be:

Char ::= #x9 | #xA | #xD | [#x20-#x7e]

Don't allow quoted names to be empty

Currently (v0.2.0) it is allowed an empty quoted string to be a symbol. This is undesirable for most applications.

Therefore, instead of:

QuotedName ::= ('"' [^"\n\t\r]* '"') | ("'" [^'\n\t\r]* "'")

It should be:

QuotedName ::= ('"' [^"\n\t\r]+ '"') | ("'" [^'\n\t\r]+ "'")

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.