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' |