All the steps for setting up thinkfan
on thinkpad x1 yoga gen 7:
-
install sensors (likely)
-
install thinkfan
-
create config file for driver (or whatever it is):
#!/bin/bash | |
# Run two processes of tlsf-sdf in parallel: | |
# - one for the original spec, | |
# - one for the dualized spec. | |
# All agruments are relayed to tlsf-sdf-opt. | |
set -m # enable 'job control' |
#!/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 |
" 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 |
#!/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: |
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 |
# 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) |
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]: |
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 subprocess | |
import sys | |
if sys.version_info < (3, 0): | |
# python2.7 version | |
def execute_shell(cmd, input=''): | |
""" | |
:param cmd: | |
:param input: sent to sdtin |