bisimulation check using cfsm_bisimulation from Diego's thesis

.github/workflows/main.yml

@@ -19,7 +19,14 @@ jobs:
       with:
         go-version: ${{ matrix.go-version }}
     - name: Checkout code
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
+    - name: Setup Python
+      uses: actions/setup-python@v5
+      with:
+        python-version: '3.12'
+        cache: 'pip' # caching pip dependencies
+    - name: Install cfsm_bisimulation
+      run: pip install -r requirements.txt
     - name: Test
       run: go test ./... -coverprofile=coverage.txt -covermode atomic -coverpkg=./cfsm/...,./internal/...,./contract -timeout 30s
     - name: Print coverage info
@@ -30,7 +37,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
     - name: Checkout code
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
     - name: Install Go
       uses: actions/setup-go@v4
       with:

Dockerfile

@@ -24,8 +24,21 @@ RUN --mount=type=cache,target=/home/$USERNAME/.cache/go-build \
     go build -v -o /usr/local/bin/middleware cmd/middleware/middleware.go
 
 # FROM scratch AS prod
-# RUN GRPC_HEALTH_PROBE_VERSION=v0.4.22 && \
-#     wget -qO/bin/grpc_health_probe https://github.com/grpc-ecosystem/grpc-health-probe/releases/download/${GRPC_HEALTH_PROBE_VERSION}/grpc_health_probe-linux-amd64 && \
-#     chmod +x /bin/grpc_health_probe
+# ENV PATH=/
+# COPY --from=dev /bin/grpc_health_probe /
 # COPY --from=dev /usr/local/bin/middleware /
 # COPY --from=dev /usr/local/bin/broker /
+
+
+# Use Python 3.12 as base image
+FROM python:3.12 as with-python-vfsm-bisimulation
+ENV PYTHONUNBUFFERED=1
+
+# Set working directory to /app
+WORKDIR /app
+
+RUN pip install z3-solver cfsm-bisimulation
+
+COPY --from=dev /bin/grpc_health_probe /usr/local/bin/
+COPY --from=dev /usr/local/bin/middleware /usr/local/bin/
+COPY --from=dev /usr/local/bin/broker /usr/local/bin/

LICENSE

@@ -0,0 +1,28 @@
+BSD 3-Clause License
+
+Copyright (c) 2024, Pablo Montepagano
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+   list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice,
+   this list of conditions and the following disclaimer in the documentation
+   and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its
+   contributors may be used to endorse or promote products derived from
+   this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

LOGDESCRIPTION.md

@@ -0,0 +1,54 @@
+# SEArch logs description
+
+In their current state, logs only meet the basic requirement for debugging purposes. Logs mainly allow basic monitoring of communication messages between components and are split in four categories:
+
+1. **middleware - broker:** encompases messages sent or received between a middleware and the broker, for example:
+
+*A Middleware logs it's view of a brokerage request to the Broker:*
+```
+     middleware-client:10000 - Requesting brokerage of contract
+```
+
+2. **service/client - middleware:** encompases messages exchanged between agents participating in an execution and their corresponding middlewares. Examples of these events are: 
+
+*A Middleware logs it's view of a message sent by a process running behind it:*
+```
+     Received CardDetailsWithTotalAmount: {232 22 22 110}
+```
+
+3. **middleware - middleware:** encompases the logging events associated to messages exchanged between middlewares, for example:
+
+*A Middleware logs when it dispatches a message to a another middleware hosting a remote participant:*
+```
+     Sent message to remote Service Provider for channel cf4ea1f5-44d3-4b27-b489-64c424911611, participant PPS
+```
+
+4. **critical internal actions of the infrastructure's component:** these messages are used for monitoring the behaviour of the components by following their execution by tracking chosen internal actions, for example: 
+
+*A Middleware logs when it receives a first outbound message from a participant:*
+```
+     Received first outbound message to send on channel cf4ea1f5-44d3-4b27-b489-64c424911611 for participant Srv. Opening connection to remote Service Provider.
+```
+*A Middleware starts the routine that periodically sends outgoing messages on an outbox buffer:*
+```
+     Started sender routine for channel cf4ea1f5-44d3-4b27-b489-64c424911611, participant Srv
+```
+
+Several debugging entries of logs can be found in the code. These entries are used to get a close look at critical parts of the code implementing the different components, both of the infrastructure, and the example provided with the implementation.
+
+## Logs when running within Docker containers
+
+As we mentioned before, *SEArch* has a basic logging infrastructure based on using the standard output stream of the processes. 
+
+When running within a Docker container it is possible to obtain and visualize the logs by using built in capability of the `docker compose` pluggin.
+
+For a basic usage of this infrastructure a user can try the following commands:
+
+1. Visualizing the a time based composition of all the containers:
+```bash
+     docker compose logs -f
+```
+2. Visualizing the log of a specific container:
+```bash
+     docker compose logs [container_identifier]
+```