Os 4 exemplos contêm uma mesma maquina de estados e diferentes propriedades.
Os numeros no nome dos arquivos descrevem quais estados não satisfazem a prioridade. Modelo e propriedades validados usando NuSMV
| ; This example illustrates basic arithmetic and | |
| ; uninterpreted functions | |
| (declare-fun x () Int) | |
| (declare-fun y () Int) | |
| (declare-fun z () Int) | |
| (declare-fun gcd3 (Int Int Int) Int) | |
| (declare-fun gcd2 (Int Int) Int) | |
| (declare-fun result () Int) |
| \usepackage{subcaption} | |
| %... | |
| \begin{figure}[htb] | |
| \caption{Examples of Figures} | |
| \label{fig:test} | |
| \begin{subfigure}{.5\linewidth} | |
| \centering |
| 4 | |
| 1 2 p q 2 2 3 | |
| 2 2 p r 2 2 4 | |
| 3 2 q r 1 1 | |
| 4 1 q 1 4 | |
| ( AF ( EX ( q ) -> AF ( p ) ) ) |
Os 4 exemplos contêm uma mesma maquina de estados e diferentes propriedades.
Os numeros no nome dos arquivos descrevem quais estados não satisfazem a prioridade. Modelo e propriedades validados usando NuSMV
| %DIF PREAMBLE EXTENSION ADDED BY LATEXDIFF | |
| %DIF UNDERLINE PREAMBLE %DIF PREAMBLE | |
| \usepackage[normalem]{ulem} | |
| \RequirePackage{color} \definecolor{RED}{rgb}{1,0,0} \definecolor{BLUE}{rgb}{0,0,1} %DIF PREAMBLE | |
| \DeclareRobustCommand{\hsout}[1]{\texorpdfstring{\sout{#1}}{#1}} | |
| \providecommand{\DIFadd}[1]{{\protect\color{blue}{#1}}} %DIF PREAMBLE | |
| \providecommand{\DIFdel}[1]{{\protect\color{red}\hsout{#1}}} %DIF PREAMBLE | |
| %DIF SAFE PREAMBLE %DIF PREAMBLE | |
| \providecommand{\DIFaddbegin}{} %DIF PREAMBLE | |
| \providecommand{\DIFaddend}{} %DIF PREAMBLE |
| package br.usp.icmc.labes.mealyInference; | |
| import java.io.File; | |
| import java.util.ArrayList; | |
| import java.util.List; | |
| import java.util.Random; | |
| import br.usp.icmc.labes.mealyInference.utils.IrfanEQOracle; | |
| import br.usp.icmc.labes.mealyInference.utils.Utils; | |
| import de.learnlib.algorithms.lstar.ce.ObservationTableCEXHandler; |
| #!/usr/bin/env python | |
| # ============================================================================== | |
| # -- find carla module --------------------------------------------------------- | |
| # ============================================================================== | |
| import glob | |
| import os | |
| import sys |
| import evdev | |
| from evdev import ecodes, InputDevice | |
| device = evdev.list_devices()[0] | |
| evtdev = InputDevice(device) | |
| val = 65535 # val \in [0,65535] | |
| evtdev.write(ecodes.EV_FF, ecodes.FF_AUTOCENTER, val) |
| sudo apt install libcanberra-gtk-module libcanberra-gtk3-module |
| import numpy as np | |
| import os | |
| import cv2 | |
| # source | |
| # https://www.codingforentrepreneurs.com/blog/how-to-record-video-in-opencv-python/ | |
| filename = 'video.avi' | |
| frames_per_second = 24.0 | |
| res = '720p' |