Automatic Update

.gitignore

@@ -13,3 +13,4 @@ _api.so
 venv
 htmlcov
 .coverage
+.DS_Store

README.md

@@ -3,28 +3,68 @@ Intre**py**d is a **python** module that provides a simulator and a model checke
 a rich API, to allow the rapid prototyping of **formal methods** algorithms
 for the rigorous analysis of circuits, specifications, models.
 
-## Installation
+# Index
+1. [Installation](#installation)
+    1. [Officially Supported OSes](#officially-supported-oses)
+    1. [Prerequisites](#prerequisites)
+    1. [Install via pip](#install-via-pip)
+    1. [Install via setup.py](#install-via-setup.py)
+1. [Quick Start](#quick-start)
+    1. [Constructing Models](#constructing-models)
+    1. [Simulating Models](#simulating-models)
+    1. [Model Checking](#model-checking)
+    1. [Benchmarking](#benchmarking)
+    1. [Model Checking in the Cloud](#model-checking-in-the-cloud)
+1. [Resources](#resources)
+    1. [Formal Methods Little Corner](#formal-methods-little-corner)
+    1. [Bug reporting](#bug-reporting)
+    1. [Feedback](#feedback)
+
+# Installation
 Intrepyd is available from PYPI [here][2]. It can be installed simply with
 ```
 pip3 install intrepyd
 ```
 issued from a terminal.
 
-### Officially Supported OSes 
+## Officially Supported OSes
 - Windows 10 or above
 - Ubuntu 19.04 or above
 
-### Prerequisites
-- python 3.7
+## Prerequisites
+- python 3.8 (exactly this version)
+- (Windows only) [Visual C++ Redistributable for Visual Studio][1]
+
+## Install via pip
+TODO
+
+## Install via setup
+TODO
+
+# Quick start
+
+## Constructing Models
+TODO
+
+## Simulating Models
+TODO
+
+## Model Checking
+TODO
+
+## Benchmarking
+TODO
+
+## Model Checking in the Cloud
+TODO
 
-### Prerequisites for Windows only
-- [Visual C++ Redistributable for Visual Studio][1]
+# Resources
 
 ## Formal Methods Little Corner
 A collection of experiences using Intrepyd can be found [here](https://formalmethods.github.io).
 
 ## Bug reporting
-Please report any bug you should experience [here](https://github.com/formalmethods/intrepyd/issues).
+Please report any bug you should experience [here](https://github.com/formalmethods/intrepid/issues).
 
 ## Feedback
 If you wish to drop a feedback you may write to

VERSION

@@ -1 +1 @@
-0.10.0
+0.10.1

app/__init__.py

@@ -0,0 +1,3 @@
+"""
+App
+"""

app/inputs.py

@@ -1,13 +1,7 @@
 """
-Copyright (C) 2021 Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-
-This file is distributed under the terms of the 3-clause BSD License.
-A copy of the license can be found in the root directory or at
-https://opensource.org/licenses/BSD-3-Clause.
-
-Author: Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-  Date: 08/02/2021
+APIs for inputs
 """
+
 from flask import Blueprint, request
 
 ir = Blueprint('inputs', __name__)

app/tests/__init__.py

@@ -0,0 +1,3 @@
+"""
+Tests
+"""

app/tests/test_contexts.py

@@ -1,13 +1,7 @@
 """
-Copyright (C) 2021 Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-
-This file is distributed under the terms of the 3-clause BSD License.
-A copy of the license can be found in the root directory or at
-https://opensource.org/licenses/BSD-3-Clause.
-
-Author: Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-  Date: 08/02/2021
+APIs for context
 """
+
 import intrepid
 import unittest
 from intrepid import PREFIX

app/tests/test_engines.py

@@ -1,13 +1,7 @@
 """
-Copyright (C) 2021 Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-
-This file is distributed under the terms of the 3-clause BSD License.
-A copy of the license can be found in the root directory or at
-https://opensource.org/licenses/BSD-3-Clause.
-
-Author: Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-  Date: 08/02/2021
+APIs for engines
 """
+
 import intrepid
 import unittest
 from intrepid import PREFIX

app/tests/test_inputs.py

@@ -1,13 +1,3 @@
-"""
-Copyright (C) 2021 Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-
-This file is distributed under the terms of the 3-clause BSD License.
-A copy of the license can be found in the root directory or at
-https://opensource.org/licenses/BSD-3-Clause.
-
-Author: Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-  Date: 08/02/2021
-"""
 import intrepid
 import unittest
 from intrepid import PREFIX

app/tests/test_latches.py

@@ -1,13 +1,3 @@
-"""
-Copyright (C) 2021 Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-
-This file is distributed under the terms of the 3-clause BSD License.
-A copy of the license can be found in the root directory or at
-https://opensource.org/licenses/BSD-3-Clause.
-
-Author: Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-  Date: 08/02/2021
-"""
 import intrepid
 import unittest
 from intrepid import PREFIX

app/tests/test_nets.py

@@ -1,13 +1,3 @@
-"""
-Copyright (C) 2021 Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-
-This file is distributed under the terms of the 3-clause BSD License.
-A copy of the license can be found in the root directory or at
-https://opensource.org/licenses/BSD-3-Clause.
-
-Author: Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-  Date: 08/02/2021
-"""
 import intrepid
 import unittest
 from intrepid import PREFIX

app/tests/test_simulators.py

@@ -1,13 +1,3 @@
-"""
-Copyright (C) 2021 Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-
-This file is distributed under the terms of the 3-clause BSD License.
-A copy of the license can be found in the root directory or at
-https://opensource.org/licenses/BSD-3-Clause.
-
-Author: Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-  Date: 08/02/2021
-"""
 import intrepid
 import unittest
 from intrepid import PREFIX

app/tests/test_upload.py

@@ -1,13 +1,3 @@
-"""
-Copyright (C) 2021 Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-
-This file is distributed under the terms of the 3-clause BSD License.
-A copy of the license can be found in the root directory or at
-https://opensource.org/licenses/BSD-3-Clause.
-
-Author: Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-  Date: 27/03/2021
-"""
 import intrepid
 import unittest
 from intrepid import PREFIX

app/upload.py

@@ -1,13 +1,7 @@
 """
-Copyright (C) 2021 Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-
-This file is distributed under the terms of the 3-clause BSD License.
-A copy of the license can be found in the root directory or at
-https://opensource.org/licenses/BSD-3-Clause.
-
-Author: Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-  Date: 27/03/2021
+APIs for upload
 """
+
 from flask import Blueprint, request
 from werkzeug.utils import secure_filename
 from intrepyd.parser import ParseError, Parser

benchmarks/kind2_benchmarks.py

@@ -1,16 +1,8 @@
 """
-Copyright (C) 2017 Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-
-This file is distributed under the terms of the 3-clause BSD License.
-A copy of the license can be found in the root directory or at
-https://opensource.org/licenses/BSD-3-Clause.
-
-Author: Roberto Bruttomesso <roberto.bruttomesso@gmail.com>
-  Date: 19/01/2021
-
-Unit tests for lustre parser
+Script for runnid kind2 benchmarks
 """
-import helper
+
+from helper import from_fixture_path
 from os.path import join
 from intrepyd.lustre2py import translator
 from intrepyd.engine import EngineResult
@@ -19,7 +11,7 @@
 import multiprocessing as mp
 import time
 
-PATH_TO_KIND2_BENCHMARKS_ROOT = helper.from_fixture_path('kind2-benchmarks/')
+PATH_TO_KIND2_BENCHMARKS_ROOT = from_fixture_path('kind2-benchmarks/')
 
 def worker_br(q):
     """
@@ -86,22 +78,13 @@ def worker_bmc_ti(q):
             if eng_result == EngineResult.REACHABLE:
                 result = 'Invalid'
                 break
-            elif eng_result == EngineResult.UNREACHABLE:
+            if eng_result == EngineResult.UNREACHABLE:
                 result = 'Valid'
                 break
     except Exception as e:
         result = 'Exception ' + str(e)
     q.put([result, time.time() - start])
 
-def killer(proc_name):
-    """
-    Kills the process whose name is proc_name
-    """
-    for proc in psutil.process_iter():
-        if proc.name() == proc_name:
-            proc.kill()
-            break
-
 def run_with_timeout(timeout, tool):
     """
     Runs a benchmark with a time limit
@@ -136,7 +119,8 @@ def test_benchmark():
                     name = fname[pos:]
                     translator.translate(fname, 'top', 'encoding.py', 'real')
                     time.sleep(1) # Give some extra time to write encoding.py to a file
-                    for engine in ['br', 'bmc', 'bmc_ti']:
+                    # for engine in ['br', 'bmc', 'bmc_ti']:
+                    for engine in ['br']:
                         print('[{:3}/848] {} {}'.format(count, name, engine), end='')
                         res, elapsed = run_with_timeout(5, engine)
                         print(' {} {}'.format(res, elapsed))