Skip to content
Snippets Groups Projects
Commit c24dc165 authored by Jaime Arias's avatar Jaime Arias
Browse files

update README

parent 3b4b5cf3
No related branches found
No related tags found
No related merge requests found
......@@ -26,23 +26,21 @@ It takes as input an [`Imitator`](https://www.imitator.fr/) model and returns an
specification.
```
python3 app.py --help
usage: app.py [-h] [--output OUTPUT] [--collapsing | --no-collapsing] --input INPUT
λ> python3 app.py -h
usage: app.py [-h] [--output OUTPUT] --input INPUT
From Imitator to Maude specifications
options:
-h, --help show this help message and exit
--output OUTPUT Maude output file (default: ./model.maude)
--collapsing, --no-collapsing
Use collapsing approach (default: False)
--input INPUT Imitator file (default: None)
-h, --help show this help message and exit
--output OUTPUT Maude output file (default: ./model.maude)
--input INPUT Imitator file (default: None)
```
Next, an example of use:
```
python3 app.py --no-collapsing --input tests/examples/ex1x.imi
python3 app.py --input tests/examples/coffee.imi
```
## Running Test
......
import argparse
from src.Parser import CollapsingParser, InterpreterParser, NoCollapsingParser
from src.Parser import InterpreterParser
def main(input_filename, output_filename):
......
import os
import re
import textwrap
from abc import ABC, abstractmethod
import antlr4
from src.dist.ImitatorLexer import ImitatorLexer
from src.dist.ImitatorParser import ImitatorParser
from src.Imitator import Automaton, Location, Model, Transition
from src.Imitator import Automaton, Model, Transition
from src.ImitatorVisitor import MyVisitor
from src.Maude import ImportType, Maude
class Parser(ABC):
"""
An abstract class to represent the parser of Imitator
Attributes
----------
maude : Maude
Object containing methods to generate Maude statements
"""
def __init__(self) -> None:
"""Constructor of the class"""
self.maude = Maude()
@abstractmethod
def to_maude(self, model: Model) -> str:
"""Parse Imitator model to Maude model"""
pass
def parse_file(self, filename: str) -> str:
"""
Parse an Imitator file into a Maude model
Parameters
----------
filename : str
Imitator file
sync_product : bool
Computes the synchronisation product of the automata
Returns
-------
str
"""
fs_in = antlr4.FileStream(filename, encoding="utf8")
# lexer
lexer = ImitatorLexer(fs_in)
stream = antlr4.CommonTokenStream(lexer)
# parser
parser = ImitatorParser(stream)
tree = parser.main()
# evaluator
visitor = MyVisitor()
model = visitor.visit(tree)
# parse to Maude
output = self.to_maude(model)
return output
class InterpreterParser(Parser):
class InterpreterParser:
"""A class to represent the parser of Imitator to Maude using the interpreter version"""
def __init__(self) -> None:
"""Constructor of the class"""
super().__init__()
self.maude = Maude()
def _get_parameter_constraints(self, model) -> list[str]:
"""Get the initial constraints of parameters
......@@ -440,3 +383,38 @@ class InterpreterParser(Parser):
"""
return textwrap.dedent(model_str).strip()
def parse_file(self, filename: str) -> str:
"""
Parse an Imitator file into a Maude model
Parameters
----------
filename : str
Imitator file
sync_product : bool
Computes the synchronisation product of the automata
Returns
-------
str
"""
fs_in = antlr4.FileStream(filename, encoding="utf8")
# lexer
lexer = ImitatorLexer(fs_in)
stream = antlr4.CommonTokenStream(lexer)
# parser
parser = ImitatorParser(stream)
tree = parser.main()
# evaluator
visitor = MyVisitor()
model = visitor.visit(tree)
# parse to Maude
output = self.to_maude(model)
return output
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment