Skip to content

Instantly share code, notes, and snippets.

@5nizza
5nizza / smt2.vim
Created September 28, 2013 18:44
Slightly modified version of Roberto Vigo's smt2 syntax file for vim.
" Vim syntax file
" Language: SMT-LIB
" Maintainer: Roberto Vigo
" Latest Revision: 23 Jan 2012
if exists("b:current_syntax")
finish
endif
" Keywords
#!/bin/bash
# the source: http://serverfault.com/questions/515833/how-to-remove-private-key-password-from-pkcs12-container
if [ $# -ne 2 ]
then
echo "Usage: `basename $0` YourPKCSFile YourPKCSPassword"
exit $E_BADARGS
fi
@5nizza
5nizza / shell.py
Last active October 18, 2015 15:02
Execute shell command, sending input if provided
import subprocess
import sys
if sys.version_info < (3, 0):
# python2.7 version
def execute_shell(cmd, input=''):
"""
:param cmd:
:param input: sent to sdtin
@5nizza
5nizza / bdd_to_smt.py
Last active October 18, 2015 15:41
Convert CUDD's BDD into SMT formula. Naive way -- defines function for each node. Careful -- not tested.
class Function(object):
def __init__(self, name, input_args, body):
self.body = body
self.input_args = input_args
self.name = name
def smt_call(self, val_by_arg=None):
args_ = ' '.join(val_by_arg[a] if val_by_arg else a
for a in self.input_args)
return '({name} {args})'.format(name=self.name, args=args_)
import spot
import buddy
from typing import Set
from helpers.str_utils import remove_from_str
from interfaces.automata import Label, LABEL_TRUE
from interfaces.expr import Signal
def parse_bdd(bdd:buddy.bdd, d:spot.bdd_dict) -> Set[Label]:
@5nizza
5nizza / gen_edges_fun_smt.py
Created March 22, 2017 17:25
Generate SMT define-fun from graph edges list
# the main function
def get_edges_as_smt(function_name:str, a1:str, a2:str, node_type:str, graph):
or_components = []
for s, d_list in graph.items():
for d in d_list:
or_components.append('(and (= {a1} {s}) (= {a2} {d}))'.format(a1=a1,a2=a2,s=node_type+str(s),d=node_type+str(d)))
or_smt = '(or %s)' % (' '.join(or_components))
return '(define-fun {function_name} (({a1} {node_type}) ({a2} {node_type})) Bool {body})'.format(
a1=a1, a2=a2, node_type=node_type, function_name=function_name, body=or_smt)
@5nizza
5nizza / lts_to_spot.py
Created March 26, 2017 18:34
Conversion from PARTY LTS into the SPOT automaton
from itertools import chain
from typing import Union
import spot
import buddy
from interfaces.automata import Label
from interfaces.lts import LTS
from synthesis.funcs_args_types_names import ARG_MODEL_STATE
@5nizza
5nizza / sort_by_last_modified_content.py
Last active March 24, 2018 16:49
Sort directories by last modified date of its files
#!/usr/bin/env python3
import argparse
import os
from os.path import join
from datetime import datetime
# https://stackoverflow.com/a/287944/801203
class Colors:
@5nizza
5nizza / tlsf.vim
Last active September 21, 2018 16:58
Syntax file for TLSF SYNTCOMP format
" Vim syntax file
" Language: TLSF
" Maintainer: Ayrat Khalimov <ayrat.khalimov@gmail.com>
" Last change: Sep 20, 2018
"
" put this into to your ~/.config/nvim/init.vim
"
" augroup syntax
" au BufRead,BufNewFile,BufNewFile *.tlsf setfiletype tlsf
" augroup END
@5nizza
5nizza / mc.sh
Created January 24, 2021 14:08
TLSF model checker using IIMC
#!/usr/bin/bash
# This script model checks a given AIGER file wrt. TLSF specification:
# @return: 0 on success, non-zero on failure
# Convert TLSF to AIGER monitor:
# syfco --format smv -m fully example.tlsf | smvtoaig > monitor.aag
# Combine monitor with implementation:
# combine-aiger monitor.aag implementation.aag > combined.aag