Thursday, January 17, 2019

Installing z3py

The Z3 Python API requires the following environment variables to be set up.
  • The PATH or LD_LIBRARY_PATH variables needs to poin to the directory containing "libz3.dll" or "libz3.so"
  • The PYTHONPATH environment variable needs to point to the directory that contains "z3/z3.py"
If you obtained the Z3 distribution as part of our binary release zip files, which you unzipped into a directory called "MYZ3", then follow these instructions to update the environment variables:
Windows:
set PATH=%PATH%;MYZ3\bin
set PYTHONPATH=MYZ3\bin\python
Linux:
export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:MYZ3/bin
export PYTHONPATH=MYZ3/bin/python
On Ubuntu, even if you have installed z3py through `apt install python-z3`, you still need to manually setup the paths as follows:
export LD_LIBRARY_PATH=/usr/lib/x86_64-linux-gnu
export PYTHONPATH=/usr/lib/python2.7/dist-packages/z3

Sunday, December 30, 2018

Adjusting video/audio sync with ffmpeg

If you need to delay video by 3.84 seconds, use a command like this:
ffmpeg.exe -i "movie.mp4" -itsoffset 3.84 -i "movie.mp4" -map 1:v -map 0:a -c copy "movie-video-delayed.mp4"
If you need to delay audio by 3.84 seconds, use a command like this:
ffmpeg.exe -i "movie.mp4" -itsoffset 3.84 -i "movie.mp4" -map 0:v -map 1:a -c copy "movie-audio-delayed.mp4"
Make sure, that your ffmpeg build is not too old, newer than 2012 will suffice.

Explanation
-itsoffset 3.84 -i "movie.mp4"
Offsets timestamps of all streams by 3.84 seconds in the input file that follows the option (movie.mp4).
-map 1:v -map 0:a
Takes video stream from the second (delayed) input and audio stream from the first input - both inputs may of course be the same file.
A more verbose explanation can be found here:
http://alien.slackbook.org/blog/fixing-audio-sync-with-ffmpeg/

Reference

https://superuser.com/questions/982342/in-ffmpeg-how-to-delay-only-the-audio-of-a-mp4-video-without-converting-the-au

Thursday, August 24, 2017

A note on rational vs regular vs automatic relations

In this post, all relations are over finite words with finite alphabets.

Automatic relations. A regular n-ary relation can is the set of n-tuples recognisable by a DFA over $\Sigma^n$. Hence all words related by a regular relation have the same length. Automatic relations are regular relations augmented with a special symbol $\bot$ that is used to indicate tail spaces. For example, a binary automatic relation $R$ relates two words $w$ and $w'$ iff $(w\bot^n,w'\bot^m)\in R$ for all $n,m\ge 0: |w|+n=|w'|+m$. In this way an automatic binary relation allows for the existence of an infinite sequence $w_0,w_1,...$ with $w_0\ R\ w_1\ R\ w_2...$ and $|w_0|<|w_1|<...$.
Examples. The following binary relations are automatic: lexicographic ordering, bitwise operations on binary strings, rational number ordering, "a subword of" over a unary alphabet, length ordering, and the edge relation of the configuration space of a TM.
Automatic structures. Recall that a structure $A$ is a tuple $(D; R_1, . . . , R_m)$ where $D$ is a non-empty set called the domain and $R_1,...,R_m$ are basic (or atomic) relations on $D$.
Theorem. (Hodgson 1982) The first-order theory of any automatic structure is decidable.
More precisely, there is an algorithm that given a FO formula $\phi(x_1,...,x_n)$ and an automatic structure $A$, produces a DFA $A_\phi$ recognising the tuples $(a_1,...,a_n)$ that satisfies the formula in $A$. This can be shown by induction on the structure of the formula, using the fact that automata recognisable relations are closed under the Boolean operations and the projection operations. This automata construction also indicates a connection between automatic structures and FO-definable structures, namely,
Corollary. A structure first-order definable in an automatic structure is automatic.

Rational & regular relations. Rational relations are language recognised by finite state transducers over alphabet $(\Sigma\cup\{\epsilon\})\times(\Sigma\cup\{\epsilon\}).$ Rational relations can encode computations of TMs. Regular relations are exactly the rational relations that preserve lengths.
Examples. The following relations are rational but not automatic: "a subword of", "a prefix of", etc.
Fact. Determinisation of transducer is not always possible and the result may not be unique. In fact it is undecidable as for whether a rational relation has a deterministic transducer.
Fact. Rational relations are not closed under complementation and intersection.
Fact. A rational relation can be recognised by a finite transducer on $(\Sigma_\epsilon)\times(\Sigma_\epsilon)$.

Resources

1. Uniformization in Automata Theory, Arnaud Carayol
2. Three Lectures on Automatic Structures, Bakhadyr Khoussainov and Mia Minnes.

Wednesday, June 14, 2017

While programs

Fact. Every while program can be simulated by while program with at most one while loop.

Harel's proof using structural induction
Kozen's proof using KAT
Kleene Algebra with Tests (KAT)
Kozen's lecture notes on KAT
Kozen's result about the complexity & decidability of KAT

Wednesday, May 17, 2017

Building a VS2013 C# project in a VS2015+ environment

Q: Warning about missing Nuget packages on compiling
A: Remove the error emitting lines in the csproj files as indicated here.

Q: ArgumentException: XXX.dll doesn't contain any UserControl types on execution
A: Mark the project containing the main program as the StartUp project.