Saturday, December 14, 2013

Commands on File Compression and Decompression

zip

zip -r foo.zip [directory]
unzip foo.zip

tar

tar -cvf foo.tar [directory]
tar -xvf foo.tar

tar.gz

tar -zcvf foo.tar.gz [directory]
tar -zxvf foo.tar.gz
tar -zxvf foo.tar.gz -C [directory]

.bz2

tar -jcvf foo.tar.bz2 [directory]
tar -xvjpf foo.tar.bz2

Monday, November 18, 2013

Apache2 Notes

Enabling a module

On seeing this error:

.htaccess: Invalid command 'RewriteEngine'

This indicates that rewrite module is not enabled. In Apache 2, both module and sites are handled in the separated folders under /etc/apache2:

mods-available/
mods-enabled/
sites-available/
sites-enabled/

In the *-available folders are the configurations to be used, for instance, here we need to enable rewrite module, we just type

sudo a2enmod rewrite

You see that rewrite.load is in the folder mods-available with the content:

LoadModule rewrite_module /usr/lib/apache2/modules/mod_rewrite.so

You will be notified to restart/reload the Apache service. Do it.

Enabling a website

We write the configurations as foo.com in sites/available:

<VirtualHost 127.0.0.3:80>
        ServerAdmin webmaster@example.com
        ServerName  localhost
        ServerAlias foo.com

        # Indexes + Directory Root.
        DirectoryIndex index.php
        DocumentRoot /var/www/foo


        # Logfiles
        ErrorLog  /var/www/foo/logs/error.log
        CustomLog /var/www/foo/logs/access.log combined
</VirtualHost>

Make sure there is a logs folder

cd /var/www/foo
mkdir logs

And then enable the website

sudo a2ensite foo.com 

Just to notice how to disable the website:

sudo a2dissite foo.com

Most importantly, enact the changes.

sudo service apache2 restart

Troubleshooting: Does PHP have write permission to a folder?

This article only talks about PHP installed alongside Apache under Linux (see here). Since PHP is run through libapache2-mod-php5. it inherits the permissions from Apache. So let's take a look about Apache. By default, it uses www-data user, to check this,

ps -u www-data

If it is so, you might get something similar:

PID TTY          TIME CMD
 1276 ?        00:00:00 php5-fpm
 1277 ?        00:00:00 php5-fpm
 1278 ?        00:00:00 php5-fpm
 1279 ?        00:00:00 php5-fpm
14934 ?        00:00:00 apache2
14935 ?        00:00:00 apache2
14936 ?        00:00:00 apache2
...

Now check user info and its group of www-data

cat /etc/passwd | grep www-data

The following shows up on my machine which says it doesn't belong to the root group or my administrator group.

www-data:x:33:33:www-data:/var/www:/bin/sh

We list the file permissions of the folder img/ to see apache's right:

ls -l | grep img

All right! Since Apache is in other group here, it doesn't have 'w' permission.

drwxrwxr-x 2 admin admin 4096 Nov 12 19:26 img

Then let's give him the permission. Notice that it is dangerous to do this, since in this way every user on the computer will have rights on this folder. Normally, we let the owner of the folder be Apache, and others can only read.

chmod o+w img
References

Sunday, November 17, 2013

MS Windows Terminology Italian - English

La Terminologia principale del MS Windows in correspondenza fra italiano e inglese. The correspondence of MS Windows terminology between Italian and English.

account utente User account
aggiornamento update
arresta il sistema shut down
attendere wait
attivazione o disattivazione activation or disactivation
avviare start
barre degli strumenti Tool bar
caricamento loading
cerca search
collegamenti shortcuts
connessioni di rete Network connection
Disinstalla o modifica programma Uninstall or modify programs
disinstalla uninstall
eseguire execute
gestione attività Task manager
Gestione dispositivi Device Manager
ibernazione hibernate
Immagini Pictures
impostazioni configuration
indrizzi address
manutenzione maintainance
Modalità provvisoria Safe Mode
mostra desktop show desktop
nuova new
Pannello di controllo Control Panel
proprietà property
riavvia il sistema restart
risoluzione problemi Troubleshooting
Sistema e sicurezza System and Security
souni sound
stampante printer
strumento tool

To sort a random file by alphabet,

sort -gk 2 temp

Saturday, October 19, 2013

Fan Cleaning: DELL INSPIRON 1564

Don't force it, there must be a screw under.
One screwdriver undoes all the screws, what a design!
Most overheating problems are caused by an untidy fan.

STEPS

  1. Prepare two sheets of paper, 1 pen, 1 Philips screwdriver (better lightly magnetized), 1 thin small blade, 1 brush, some tissue paper. You workbench should be long, wide and clean. Put a tidy cloth below your computer.
  2. Close and fold the computer, detach the power adapter, unbutton the battery.
  3. Go to the back, remove the "inverted-T" part. Remind you that the three screws are attached to that piece and can't be removed from it. You can now see your memory chips, hard-drive, Wi-Fi chip with two wires (black and white), CMOS battery. Remove wifi wires.
  4. Now draw a map of all the screws on the back, remove all the screws and place them exactly where they shall be on the map.

    click to enlarge

  5. Take the CD-drive out (it is now free). You see three screws on the rim, draw them on the map, and do the same as for the others.
  6. Take the blade and slide it into the narrow space between the border of the keyboard and the metal shell. Lift it and move around to take off the border. It is locked by plastic hooks so you might hear some crack sound, it is okay. This piece is attached to the motherboard by the flat wires (power button). Lift the plastic lock to take the flat wire off. Now you get rid of it.
  7. Remove the keyboard afterwards, there are three screws so draw a small map for the keyboard too. The flat wire for the keyboard is right under it, so when you are done with screws, tilt the keyboard, undo the wire as in the last step.
  8. Here comes the piece of metal shell, it is connected to the motherboard since there is the touch-pad. Also there is the wifi wire dangling, so we'd better take the wifi wire out of its channel. Draw another map, undo all the screws as before. Use the blade again to remove the shell away. It is locked by plastic hooks too, so again there are some cracks and this time it is bit harder. But if you really feel it is tough, you might have forgotten some drew. When you are done, take off the touchpad wire and remove the whole piece.
  9. We don't need to remove the motherboard to take out the fan. Just draw a small map for the fan, first take its power wire off at the bottom. Remove the screws. There is one screw around for the main power socket, undo that as well, just to gain some space.
  10. Take the fan out and clean it with the tissue paper and the brush (you can open it, there are a couple of small screws on the back). Clean the heat sink too.
  11. Now do the reverse in the inverted order.

Friday, October 11, 2013

Everyday Shell Scripts

  • Rename the extensions of all files,

    for FILE in *.foo ; 
    do NEWFILE=`echo $FILE | sed 's/.foo/.bar/g'` ;
     mv "$FILE" $NEWFILE ; 
    done
  • Test if a variable is set (pay attention to the space, they can't be eliminated),

    if [ ! -z "$var" ]; then
      echo "var exists"
    fi
  • Test if a file exists,

    if [ -f "$file" ]; then
      echo "file exists"
    fi
  • Copy one file to the clipboard (install xclip first)

    cat file | xclip -selection c
  • Paste clipboard to a file

    xclip -o > file
  • Define a function

    foo(){
      echo "FUNCTION"
    }
    fun=$(foo)
    
  • The most recent foreground pipeline exit status: $?

    if [ $? -eq -1 ]
      then
      exit 1
    fi 
  • Several ways of for loop controlled by a var

    for I in {1..10}; do echo $I; done
    for I in 1 2 3 4 5 6 7 8 9 10; do echo $I; done
    for I in $(seq 1 10); do echo $I; done
    for ((I=1; I <= 10 ; I++)); do echo $I; done
  • Generate ticks in (-4pi, 4pi):

    for i in $(seq -4 4); do b=`echo "$i * 3.14159" | bc`; echo -ne $b","; done; 

    This is useful for PGFplots for trigonometric ticks,

    xtick={-12.56636,-9.42477,-6.28318,-3.14159,0,
    3.14159,6.28318,9.42477,12.56636},
    xticklabels={
            $-4\pi$, $-3\pi$, $-2\pi$, $-\pi$, $0$,
            $\pi$, $2\pi$, $3\pi$, $4\pi$
     }
  • Convert all jpeg files and save them as png files.

    for file in *.jpg;do 
      newfile=`echo $file | sed 's/.jpg/.png/g'`;
      gm convert -quality 60 $file $newfile;
    done
  • Compress all jpeg files.

    mkdir new
    for file in *.jpg;do 
      newfile="new/$file";
      gm convert -quality 60 $file $newfile;
    done

Friday, October 4, 2013

LaTeX Typesetting Hacks (Continuously Updating)

This list of knowledge is a collection of common problems encountered in everyday typesetting. The solution is either seen by reading package manuals of LaTeX related websites. But here I would like to give a list of clear reference (let's do it in factory mode). I've evaluated different solutions and try to make the hacks as simple as possible.

  • By default, hyperref packages creates a colorful border for links. To remove it,

    %remove colorful borders on links without updating the package
    \hypersetup{%
        pdfborder = {0 0 0}
    }
  • How to use "List of Algorithms" as toc title and "Algorithms" for single title instead of "List of Listings" while using listings package?

    %listing customization
    \renewcommand{\lstlistingname}{Algorithm}% Listing -> Algorithm
    \renewcommand{\lstlistlistingname}{List of \lstlistingname s}% List of Listings -> List of Algorithms
  • How not to break hypen in bibliography?

    %bibliography no break hypen
    \makeatletter
    \newcommand*\bibhyphen{\hbox{-}\nobreak\hskip\z@skip}
    \makeatother
    \newcommand*\bibdash{\rule[0.48ex]{2em}{0.14ex}\space}
  • How to add bibliography to the table of contents?

    \usepackage[nottoc]{tocbibind} %add bibliography to toc
  • How to use "bibliography" instead of "references"?

    \renewcommand{\refname}{Bibliography}
  • How to enlarge margin paragraph width without using geometry package since it rewrites all the default layout values?

    %set twice as default
    \setlength{\marginparwidth}{2\marginparwidth}
  • How to center texts?

    %maybe you are looking for \vspace{2cm} too?
    \begin{center}
    This is centered text.
    \end{center}
  • How to give remarks in red?

    \usepackage{color}
    %you can define a macro \remark in the preamble
    \newcommand{\remark}[1]{{\color{red}REMARK: #1}}
    %then in the document
    \remark{This is a remark in red.}
  • To include Chinese/Japanese/Korean letters or characters along with pdflatex, use CJK package. Alternatively, one can choose xelatex. See CJK Doc. Notice CJK env uses two extra options to specify the encodings and font family. One can check out supported font family by checking the folder /usr/share/texmf/tex/latex/CJK/UTF8 or similar. If the font parameter is empty, the default value given in CJK.enc will be selected. On my machine, I have c70bkai.fd installed in that folder. One can also refer install CJK support to see how to manually install a CJK font to the tex tree.

    \usepackage{CJK}
    \begin{CJK}{UTF8}{bkai}
    漢字
    \end{CJK}
    %to merge CJK with another environment, embed that environment within CJK, such as
    \begin{CJK}{UTF8}{bkai}
    \marginpar{
    丁香
    }
    \end{CJK}
  • An example of including a centered figure with caption and label.

    \usepackage{grahpicx}
    \begin{figure}[ht]
    \centering
    \includegraphics{pic.jpg}
    \caption{sample picture}
    \label{fig:sample-pic}
    \end{figure}
  • How to put two pictures side by side with each of its own caption and label?

    \usepackage{subfigure}
    \begin{figure}[ht]
    \centering
    \subfigure[Caption a]{
    \includegraphics[width=.45\linewidth]{img1.png}
    \label{fig:imga}
    }
    \hspace{.2in}
    \subfigure[Caption b]{
    \includegraphics[width=.45\linewidth]{img2.png}
    \label{fig:imgb}
    }
    \caption{Two figures}%
    \label{fig:2-fig}
    \end{figure}
  • How to introduce plain codes?

    \usepackage{verbatim}
    \begin{verbatim}
    int sched_setscheduler(pid_t pid, int policy,
                           const struct sched_param *param);
    \end{verbatim}
  • How to include "Acknowledgements"?

    %do it as a section
    \section*{Acknowledgements}
    \addcontentsline{toc}{section}{Acknowledgements}
      
  • Customize figure caption. This caption will remove "Fig.", and the separator is set as space instead of the default colon.

    \renewcommand{\figurename}{}
    \usepackage[labelsep=space]{caption}

Friday, September 13, 2013

Solve Rubik's Cube in 7 Steps (with Illustrations and formulas)

Symbols: (U)p (B)ack (L)eft (R)ight (F)ront, U' means rotating in counter-clockwise direction, while U means clockwise.

Friday, September 6, 2013

Show Skype icon on top bar and launcher on Ubuntu

Problem: Skype icon not showing on panel tray (top bar) and launcher (left bar)

Affected: Ubuntu 12.04

Cause: installation from .deb

Solution:

sudo apt-get install sni-qt sni-qt:i386
gsettings get com.canonical.Unity.Panel systray-whitelist
gsettings set com.canonical.Unity.Panel systray-whitelist "['JavaEmbeddedFrame', 'Wine', 'Update-notifier', 'Skype']"

Source:

How do I Get the Skype Status Icon Back on Panel Tray

Tuesday, August 27, 2013

Scicoslab/Scipad: Upgrading from 8.70 to 8.71

Note: This guide is for Linux.

  1. Download from source
  2. Instructions are here: installation guide
  3. However, to move files from the unzipped source to the scicoslab directory ( /usr/lib/scicoslab-gtk-4.4.1/), use
  4. sudo cp -r scipad/*  /usr/lib/scicoslab-gtk-4.4.1/
    

    The lesson here is that mv command doesn't have -r option, so cp is all right.

  5. Then start scicoslab with root privilege
  6. sudo scicoslab
    
  7. Issue the following under scicoslab
  8. genlib("utillib");
    

    Exit and restart scicoslab, and that will be okay.

Tuesday, August 20, 2013

A Hands-on Guide to ScicosLab - Part 2

Define a Zero Vector

--> v = zeros(1:20)

Use Scipad Editor

To launch the embedded editor, type

--> scipad

One can write a sequence of Scicos instructions and save it as *.sci files. To load such a program into ScicosLab, type

--> exec('foo.sci');

Directory operation

It inherits a Linux style,

--> pwd
--> ls
--> cd

To clear terminal screen, use either one

--> ctrl+l
--> clc

Define a Function

For instance,

function [re,im] = compute(v, f)
    re=re+cos(2*%pi*f*v/1000000);
    im=im+sin(2*%pi*f*v/1000000);
    return [re,im];
  endfunction

The return value is a vector [re,im], as you might notice, the Scicos language is C-like but not strong-typed. This function compute takes two params. Notice that the incremental sum is not supported, that is re+=... commits an error. Once loaded into ScicosLab, it works as library functions. You can call it anytime, but after a clear command, it vanishes as all the other customized variables do.

For and While

for i=1:20, printf("%d\n",i); end

Notice that no increment of i is needed. It does so automatically at every loop.

i=1;
while i<=20, printf("%d\n",i);i++; end

TBD.

Wednesday, August 14, 2013

A Short Recap on Fourier's Toys

Fourier's building blocks were sine and cosine waves. All the majesty of periodic functions can be constructed by them.

Fourier series

Just a glimpse. A periodic function $f(x)$, with $(-\pi, \pi)$ as its basic periodic unit, can be approached by the sum of an infinite series.

$$a_0 = \frac{1}{2\pi} \int_{-\pi}^{\pi} f(x)dx \\ a_n = \frac{1}{\pi} \int_{-\pi}^{\pi} f(x)\cos(nx)dx \\ b_n = \frac{1}{\pi} \int_{-\pi}^{\pi} f(x)\sin(nx)dx \\ a_0 + \sum_{n=1}^{\infty}(a_n \cos (nx) + b_n \sin (nx))$$

Fourier Transform

Also a quick glance,

$$\mathcal{F}(f(t))(s) = \int_{-\infty}^{+\infty} f(t)e^{-2\pi i s t} dt$$

Discrete Fourier Transform (DFT)

A bit into the point. The input of DFT is a finite series of equally-spaced (in time) samples. e.g., f(0), f(0.1), f(0.2), ..., f(2π), and the output is a series of complex numbers encoding the amplitude and phase information, say $\mathcal{F}(0)$, $\mathcal{F}(F_0)$, ..., $\mathcal{F}(-F_0)$. And $F_0$ is the fundamental frequency, which is calculated as

$$F_0 = \frac{1}{N \Delta}$$

$\Delta$ is the sample period, in our example it is $0.1$. The x-axis of these numbers are the frequency spaced as in the figure below,

However, the discrete transform is thus performed, $$\mathcal{F}(n) = \sum_{k=0}^{N} f(k) e^{-2\pi i n k/N}$$

Sunday, August 11, 2013

A Hands-on Guide to ScicosLab - Part 1

The basic calculation unit is a vector or a matrix in ScicosLab. What we get used to is a 1*1 matrix.

Define a Vector

--> 0:0.1:4*%pi

Well, the result is stored in the variable ans and the vector will be displayed hereafter. This vector is comprised of float numbers from 0 to 4π with a spacing of 0.1, they are 116 numbers, check this with the function length(). Yes, %pi is the Scicos way of pre-defining some constants. For the logarithmic natural base e, it uses %e. To stop printing results after each command, one can end it with a semi-colon(;).

Use Variables

--> a = 0:0.1:4*%pi;

Variables are type-free when being declared, so the initialization will make the variable a being a vector. Any assignment will change its content and type just like using a brand-new variable. The system preserved variable ans will be updated in the same fashion after executing every command.

--> a = sin(a);

Plot a Sine Wave

--> plot(a);

This gives you a sine wave of 2 periods.

Perform Discret Fourier Transform

--> v = dft(a,-1);
--> clf();
--> plot(v);

To check the usage of a function or related entries, use

--> apropos fourier
--> help dft

To clear the graph/figure, use the function clf(). We see in the new plotting

ScicosLab just drew the real part of frequency components, to compare with the imaginary parts, use

--> plot(imag(v), 'red');

The figure gets re-shaped and we see two spikes again. As a matter of fact, the Fourier transform of sine wave is two dirac functions.

Variables Revisited

--> browsevar
--> clear

The former gives a window of currently being-used variables, and the latter command just destroys them.

Friday, August 9, 2013

Read Data Text Files into A Vector in Scicoslab

The data file temp is lines of float numbers with one at each line.

--> fp = mopen("temp","r");
--> v = mfscanf(-1,fp,"%f");
--> v';

A Note on Ubuntu Dash Icons

In principle, dash application icons are located under /usr/share/icons/hicolor/apps, however, this can be customized. For instance, the configuration for a program named ScicosLab lies in /usr/share/applications/scicoslab.desktop, it has the following content:

[Desktop Entry]
Name=ScicosLab
Comment=Scientific Computing using ScicosLab
TryExec=/usr/bin/scicoslab
Exec=/usr/bin/scicoslab
Icon=/usr/lib/scicoslab-gtk-4.4.1/config/puffin-gtk48.png
Terminal=false
Type=Application
Categories=Education;Science;Math;
StartupNotify=false
X-Desktop-File-Install-Version=0.15

One can restart the system to see the effect.

To regenerate the cache

sudo gtk-update-icon-cache --force /usr/share/icons/hicolor

Saturday, June 1, 2013

Symoblic CTL Model Checking

Ordered Binary Decision Diagram

Boolean formulas are represented in diagrams. OBDD has the following property, $$\phi \leftrightarrow \psi \Rightarrow OBDD(\phi) = OBDD(\psi)$$

Symbolic Denotation $\xi$

$\xi : S \rightarrow $boolean formulas (OBDDs). By definition, $$\xi([\phi]) := \xi(\{ s | M,s \models \phi \})$$

A list of some symbolic encodings,

  • $\xi([\mathbf{EX}\phi]) = \exists V' . (\xi ([\phi])[V'] \wedge \xi (R)[V,V'])$
  • $\xi([\mathbf{EG}\phi]) = \nu Z . (\xi([\phi]) \wedge \xi([\mathbf{EX}Z]))$
  • $\xi([\mathbf{E}(\phi\mathbf{U}\psi)]) = \mu Z . (\xi([\psi]) \vee (\xi([\phi]) \wedge \xi([\mathbf{EX}Z])))$

The above exactly parallels the classical fixed-points techniques. See a previous post (link).

Fixed-point Algorithms

The following shows the symbolic counterpart for the classical fixed points algorithms (denotational, based on states). Recall their inductive version,

  • $[\mathbf{EG}\phi]$: $X_{j+1} = X_j \cap \mathsf{PreImage}(X_j)$
  • $[\mathbf{E}(\phi\mathbf{U}\psi)]$: $X_{j+1} = X_j \cup ([\phi] \cap \mathsf{PreImage}(X_j))$
PreImage
OBDD PreImage(OBDD X){
  return ∃V'. (X[V'] ∧ ξ(R)[V,V']);
}
Check_EG
OBDD Check_EG(OBDD X) {
    Y′ := X;
    repeat
        Y := Y′;
        Y′ := Y ∧ PreImage(Y);
    until (Y′ ↔ Y);
    return Y;
}
Check_EU
OBDD Check_EU(OBDD X1 ,X2) {
    Y′ := X2;
    repeat
        Y := Y′;
        Y′ := Y ∨ (X1 ∧ PreImage(Y));
    until (Y′ ↔ Y);
    return Y;
}
Check_FairEG

Here we need to refer Emerson Lei algorithm which specifies the fair CTL version. $$ [\mathbf{E}_f \mathbf{G} \phi ] = \nu Z .([\phi] \cap \bigcap_{F_i \in FT} [\mathbf{EX}[\mathbf{E}(Z \mathbf{U}(Z \wedge F_i ))])$$

The can be interpreted as $Z$ keeps being true until all fair conditions are met when $Z$ is still true at each step of iteration.

OBDD Check_FairEG(OBDD X) {
    Z’ := X;
    repeat
        Z := Z’;
        for each Fi in FT
            Y := Check_EU(Z, Fi ∧ Z);
            Z’:= Z’ ∧ PreImage(Y);
        end for;
    until (Z’ ↔ Z);
    return Z;
}

Check Invariants

Invariants are specified as $\mathbf{AG}\phi$. Its negation is $\neg \mathbf{EF} \neg \phi$, which is a reachability issue: are there such states which can be reached from the initial states? We show the forward checking technique.

OBDD Compute_reachable() {
    Y′ := I;
    Y := ⊥;
    while ¬(Y′ ↔ Y) {
        Y := Y′;
        Y′ := Y ∨ Image(Y);
    }
    return Y;
}

Note backward checking iteratively calculates the preimage of $\phi$ until a fixed-point is reached or the preimage intersects with $I$. An advanced version with the so-called frontier (F) is presented below.

OBDD Compute_reachable() {
    Y := I;
    F := I;
    while ¬(F ↔ ⊥) {
        F := Image(F) ∧ ¬Y;
        Y := F ∨ Y;
    }
    return Y;
}

If we explain it in the set flavor, it could be at each time we only calculate the image of new states (frontier). The set of reachable states is saturated when the image of the frontier can't bring in more new states.

Forward_Check_EF

Based on the discussion above, we now can check invariants (often feature as bad behaviors).

bool Forward_Check_EF(OBDD BAD) {
    Y := F := I;
    while ¬(F ↔ ⊥) and (F ∧ BAD) ↔ ⊥ {
        F := Image(F ) ∧ ¬Y ;
        Y := Y ∨ F ;
    }
    if F = ⊥
        return false
    else
        return true
}

The above utilizes the frontier technique. It looks for all reachable states and verifies whether there are some bad states within them.

References & Readings

  1. R. Sebastiani, Symbolic CTL Model Checking, slides on Formal Methods, 2012
  2. McMillan, Symbolic Model Checking, a Carnegie-Mellon PhD dissertation, 1993
  3. Wikipedia, Fair Computational Tree Logic, http://en.wikipedia.org/wiki/Fair_computational_tree_logic

Appendix

The most of this post is heavily extracted from the RS's teaching slides, hence I don't claim the copyright. The character of this post is intended to be a note, with marginal and personal remarks. For those who need to respect the source, please read the following copy of the original copyright notice.

Copyright notice: some material (text, figures) displayed in these slides is courtesy of M. Benerecetti, A. Cimatti, P. Pandya, M. Pistore, M. Roveri, and S.Tonetta, who detain its copyright. Some exampes displayed in these slides are taken from [Clarke, Grunberg & Peled, “Model Checking”, MIT Press], and their copyright is detained by the authors. All the other material is copyrighted by Roberto Sebastiani. Every commercial use of this material is strictly forbidden by the copyright laws without the authorization of the authors. No copy of these slides can be displayed in public without containing this copyright notice.

Thursday, May 30, 2013

CTL Model Checking

Fixed-point Theory

Complete Lattice

Complete lattice is a partially-ordered set which has join ($\cup$) and meet ($\cap$) operators. The former generates the least lower bound and the latter the greatest upper bound. The state space of a Kripke model forms a complete lattice under containment, i.e. $(2^S, \subseteq)$ is a complete lattice.

Monotonic Function

$F$ is monotonic if $\forall a < b$, $F(a) < F(b)$.

Tarski's Theorem

A monotonic function over a complete lattice has the least and the greatest fixed point.

Kleene's Theorem

The mentioned fixed points can be calculated this way. Assume $F$ is a monotonic function and $\cup$-continuous (increments), the least fixed point must be reached (this chain converges): $$\emptyset \subseteq F(\emptyset) \subseteq F(F(\emptyset)) \subseteq \ldots$$

Instead, if $F$ is $\cap$-continuous (decrements), the greatest fixed point is obtained by, $$S \supseteq F(S) \supseteq F(F(S)) \supseteq \ldots$$

Formula Rewriting

All CTL formulae can be rewritten in terms of $\neg, \wedge, \mathbf{EX}, \mathbf{EU}, \mathbf{EG}$ only.

  • $\mathbf{AG}\phi = \neg \mathbf{EF} \neg \phi$
  • $\mathbf{EF}\phi = \mathbf{E}(\top \mathbf{U} \phi)$
  • $\mathbf{A}(\phi_1 \mathbf{U} \phi_2 ) = \neg \mathbf{E}(\neg \phi_2 \mathbf{U} (\neg \phi_1 \wedge \neg \phi_2 )) \wedge \neg \mathbf{EG}\neg \phi_2$
  • $\mathbf{AX} \phi = \neg \mathbf{EX} \neg \phi$

Although irrelevant at this context, but it is worthy to note that $\mathbf{EG}\phi = \mathbf{E}(\bot \mathbf{R} \phi)$, this is to say $\phi$ is never released (has to be true forever).

Tableaux Rules

  • $\mathbf{EF}\phi = \phi \vee \mathbf{EXEF}\phi$
  • $\mathbf{EG}\phi = \phi \wedge \mathbf{EXEG}\phi$
  • $\mathbf{E}(\phi \mathbf{U} \psi) = \psi \vee (\phi \wedge \mathbf{EXE}(\phi \mathbf{U} \psi))$

Pre-Image

In CTL model checking, the calculating unit is a set of states that satisfy some formula $\phi$, noted as denotation $[\phi]$. Pre-Image maps the image (in the range) back to the domain (its pre-image). It is thus defined, $$\mathsf{PreImage}([\phi]) = \{s | \exists (s, s') \in R \wedge s' \in [\phi]\}$$

$\mathsf{PreImage}$ is a monotonic function over the complete lattice $(2^S, \subseteq)$, thus Kleene's theorem applies. Pre-Image matches the idea of $\mathbf{EX}$, i.e. $[\mathbf{EX}\phi]$ is the pre-image of $[\phi]$.

Fixed points for CTL Model Checking

According to tableaux rules, $\mathbf{EG}$, $\mathbf{EF}$, $\mathbf{EU}$s are written in the form of fixed points ($\nu$: greatest, $\mu$: least.).

  • $[\mathbf{EG}\phi] = \nu Z. ([\phi] \cap [\mathbf{EX}Z])$
  • $[\mathbf{EF}\phi] = \mu Z. ([\phi] \cup [\mathbf{EX}Z])$
  • $[\mathbf{E}(\phi \mathbf{U} \psi)] = \mu Z. ([\psi] \cup ([\phi] \cap [\mathbf{EX}Z]))$

So given a CTL formula $\phi$, after rewriting, we apply the set operations for negations (complement the set) and disjunctions (union), and fixed points for temporal formulas. We say $M \models \phi$ iff $I \subseteq [\phi]$.

Tuesday, May 28, 2013

On-the-fly Construct Büchi Automata for LTL formulae

The previous post introduced the declarative construction, which is exponential. For instance, the LGBA for $p \mathbf{U} q$ has 8 states. However, on-the-fly construction can build Büchi automata for linear size. Surely, distinct automata can express the same language (further, the LTL formula).

Negative Normal Form

First we write LTL formulas into their NNF equivalence, which is composed by $\vee, \wedge, \mathbf{X}, \mathbf{U}, \mathbf{R}$ only. Negations are pushed down to literals. Here we quote some rules,

  • $\neg \mathbf{X} \phi \Rightarrow \mathbf{X} \neg \phi$
  • $\neg ( \phi \mathbf{U} \psi ) \Rightarrow (\neg \phi \mathbf{R} \neg \psi) $
  • $\neg ( \phi \mathbf{R} \psi ) \Rightarrow (\neg \phi \mathbf{U} \neg \psi) $

Tableaux Expansion

  • $\phi \mathbf{U} \psi \Rightarrow \psi \vee (\phi \wedge \mathbf{X}(\phi \mathbf{U} \psi)) $
  • $\phi \mathbf{R} \psi \Rightarrow \psi \wedge (\phi \vee \mathbf{X}(\phi \mathbf{R} \psi)) $

Disjunctive Normal Form

With all formulas converted to the following form, each disjunct is a state.

$$\bigvee_i \bigg( \bigwedge_j I_{ij} \wedge \bigwedge_k \mathbf{X}\psi_{ik} \bigg)$$

Note $\bigwedge_j I_{ij}$ represents the labels, and $\bigwedge_k \mathbf{X}\psi_{ik}$ shows the transition. When the $\mathbf{X}$-formula is not present, we write $\mathbf{X} \top$.

Cover

A cover of a set of LTL formulas $\Psi= \{ \psi_1, \ldots, \psi_k \}$ calculates the set of initial states of Büchi automaton that represents $\bigwedge_i \psi_i$. A state is denoted as $\langle \lambda, \chi, \sigma \rangle$, which are the set of labels, the next formula, the set of subformulas of satisfied in $s$.

$$\mathsf{Cover}(\Psi) := \mathsf{Expand}(\Psi, \langle \emptyset, \emptyset, \emptyset \rangle)$$

Expand

We quote its definition. Assume $s=\langle \lambda, \chi, \sigma \rangle$, $l$ is a propositional literal, $\mathsf{Expand}(\Psi, s)=$

\begin{align*} \begin{cases} s & \Psi = \emptyset \\ \emptyset & \bot \in \Psi \\ \mathsf{Expand}(\Psi \backslash \top , s) & \top \in \Psi \\ \mathsf{Expand}(\Psi \backslash \{l\}, \langle \lambda \cup \{l\}, \chi, \sigma \cup \{l\} \rangle) & l \in \Psi \\ \mathsf{Expand}(\Psi \backslash \{\mathbf{X}\psi\}, \langle \lambda , \chi \cup \{ \psi \}, \sigma \cup \{\mathbf{X}\psi\} \rangle) & \mathbf{X}\psi \in \Psi \\ \mathsf{Expand}(\Psi \cup \{\psi_1, \psi_2\} \backslash \{\psi_1 \wedge \psi_2\}, \\ \quad \quad \quad \langle \lambda, \chi, \sigma \cup \{\psi_1 \wedge \psi_2\} \rangle) & \psi_1 \wedge \psi_2 \in \Psi \\ \mathsf{Expand}(\Psi \cup \{\psi_1\} \backslash \{\psi_1 \vee \psi_2\}, \\ \quad \quad \quad \langle \lambda, \chi, \sigma \cup \{\psi_1 \vee \psi_2\} \rangle) \cup \\ \mathsf{Expand}(\Psi \cup \{\psi_2\} \backslash \{\psi_1 \vee \psi_2\}, \\ \quad \quad \quad \langle \lambda, \chi, \sigma \cup \{\psi_1 \vee \psi_2\} \rangle) & \psi_1 \vee \psi_2 \in \Psi \\ \mathsf{Expand}(\Psi \cup \{\psi_1\} \backslash \{\psi_1 \mathbf{U} \psi_2\}, \\ \quad \quad \quad \langle \lambda, \chi \cup \{\psi_1 \mathbf{U} \psi_2\}, \sigma \cup \{\psi_1 \mathbf{U} \psi_2\} \rangle) \cup \\ \mathsf{Expand}(\Psi \cup \{\psi_2\} \backslash \{\psi_1 \mathbf{U} \psi_2\}, \\ \quad \quad \quad \langle \lambda, \chi, \sigma \cup \{\psi_1 \mathbf{U} \psi_2\} \rangle) & \psi_1 \mathbf{U} \psi_2 \in \Psi \\ \mathsf{Expand}(\Psi \cup \{\psi_2\} \backslash \{\psi_1 \mathbf{R} \psi_2\}, \\ \quad \quad \quad \langle \lambda, \chi \cup \{\psi_1 \mathbf{R} \psi_2\}, \sigma \cup \{\psi_1 \mathbf{U} \psi_2\} \rangle) \cup \\ \mathsf{Expand}(\Psi \cup \{\psi_1, \psi_2\} \backslash \{\psi_1 \mathbf{R} \psi_2\}, \\ \quad \quad \quad \langle \lambda, \chi, \sigma \cup \{\psi_1 \mathbf{R} \psi_2\} \rangle) & \psi_1 \mathbf{R} \psi_2 \in \Psi \end{cases} \end{align*}

Construct $A_\phi$

With the above operations defined, we construct the Büchi Automaton for an LTL formula. $A_\phi = (Q, Q_0 , \Sigma, L, T , FT)$, with $Q_0 = \mathsf{Cover}(\{\phi\})$, $Q$ is the smallest set such that $Q_0 \subseteq Q$, also if $\langle \lambda, \chi, \sigma \rangle \in Q$, then $\mathsf{Cover}(\{\chi\}) \in Q$, the labeling function $L(s) = \{a \in \Sigma | a \models \lambda \}$, transition relation $T = \{(s,s') | s = \langle \lambda, \chi, \sigma \rangle \wedge s' \in \mathsf{Cover}(\{\chi\}) \}$, the fairness conditions $FT = \{F_1, \ldots, F_n\}$, where $F_i = \{s \in Q | \phi_i \mathbf{U} \psi_i \notin \sigma \vee \psi_i \in \sigma \}$.

Examples

Here we present the Büchi Automata built from the stated method.

Fig 1. NBA of $\mathbf{FG}p$

Fig 2. NBA of $p \mathbf{U} q$

References

  1. R. Sebastiani, Automata-theoretic LTL Model Checking, slides on Formal Methods, 2012
  2. Wikipedia, Linear temporal logic to Buchi Automaton, http://en.wikipedia.org/wiki/Linear_temporal_logic_to_Büchi_automaton

Appendix

The following is a copy of original copyright notice of slides which this article is quoting.

Copyright notice: some material (text, figures) displayed in these slides is courtesy of M. Benerecetti, A. Cimatti, P. Pandya, M. Pistore, M. Roveri, and S.Tonetta, who detain its copyright. Some exampes displayed in these slides are taken from [Clarke, Grunberg & Peled, “Model Checking”, MIT Press], and their copyright is detained by the authors. All the other material is copyrighted by Roberto Sebastiani. Every commercial use of this material is strictly forbidden by the copyright laws without the authorization of the authors. No copy of these slides can be displayed in public without containing this copyright notice.

Monday, May 27, 2013

Translate LTL formulae into Büchi Automata

LTL formulae are translated in Labelled Generalized Büchi Automata (LGBA), where labels are moved into states. See a previous post (link).

$\omega$-automaton, $\omega$-word, $\omega$-language

An $\omega$-automaton is an automaton which accepts infinite inputs. Büchi Automata are a typical example. An $\omega$-word is an accepting run on an $\omega$-automaton, the set of all $\omega$-words accepted (defined) by an $\omega$-automaton is called an $\omega$-language.

The alphabet of a language is denoted as $\Sigma$, the set of all $\omega$-words composed by symbols in $\Sigma$ is denoted as $\Sigma^{\omega}$. A language recognizable (accepted) by an automaton $A$ is written $L(A)$. Usually we only work in automata that have $L(A) \subset \Sigma^{\omega}$.

$\omega$-regular

Recall that regular languages can be recognized by NFAs/DFAs (equivalent). It can also be generated by regular grammar (left linear or right linear, but not mixed).

A language is called $\omega$-regular when it is represented as $$\bigcup_{i=1}^n U_i(V_i)^{\omega}$$

we require that $U_i$, $V_i$ be regular languages. $L$ is $\omega$-regular iff it can be recognized by Nondeterministic Büchi Automata. The $\omega$-regular languages are closed under complementation (useful for constructing $A_{\neg\phi}$).

Closures

The closure of an LTL formula is intended to calculate its components (including their negations). For instance, a closure set of $p\mathbf{U}q$ is $$\{p, q, p\mathbf{U}q, \mathbf{X}(p\mathbf{U}q), \neg p, \neg q, \neg (p\mathbf{U}q), \neg (\mathbf{X}(p\mathbf{U}q))\}$$

Atoms

An atom $A$ is called a maximal consistent subset of the closure set. First we remove negations. In order to be consistent (agree on assignments), we should have $p,q \in A$ when we have $p \wedge q \in A$. Similarly, when we have $p\mathbf{U}q \in A$, we require either $q \in A$ or $\{p \in A, \mathbf{X}(p\mathbf{U}q)\} \subset A$.

LTL to LGBA

$A_{\phi} = (Q, Q_0, \Sigma, L, T, FT)$, respectively, the set of states Q is the the set of all atoms of $\phi$, the set of initial states $Q_0$ are the atoms where $\phi$ is included, $\Sigma$ is the power set of all free variables in $\phi$, namely the alphabet, labeling function $L$ maps a state to the set of free variables appeared in that state, transition relation is built from $\mathbf{X}$-formulas, say $(\mathbf{X}\psi, \psi) \in T$, $FT$ is a set of fair conditions $\{F_1, \ldots, F_n \}$, where $$F_i = \{ s \text{ is an atom} | \psi \mathbf{U} \phi \in s \vee \phi \in s \}$$

The above is on the condition that $\psi \mathbf{U} \phi$ appears positively in $\phi$. (see Polarity)

Example

One can calculate the atoms of $p \mathbf{U} q$ and other parameters by the stated method, thus its Büchi automaton.

Fig 1. $A_{p \mathbf{U} q}$ constructed by definition

On-the-fly Construction

The above construction is called declarative construction, though an alternative is present, considering its volume, it is to be introduced in another post.

References

  1. R. Sebastiani, Automata-theoretic LTL Model Checking, slides on Formal Methods, 2012
  2. Wikipedia, ω-automaton, https://en.wikipedia.org/wiki/Ω-automaton
  3. Wikipedia, Linear temporal logic to Buchi Automaton, http://en.wikipedia.org/wiki/Linear_temporal_logic_to_Büchi_automaton

Appendix

The following is a copy of original copyright notice of slides which this article is quoting.

Copyright notice: some material (text, figures) displayed in these slides is courtesy of M. Benerecetti, A. Cimatti, P. Pandya, M. Pistore, M. Roveri, and S.Tonetta, who detain its copyright. Some exampes displayed in these slides are taken from [Clarke, Grunberg & Peled, “Model Checking”, MIT Press], and their copyright is detained by the authors. All the other material is copyrighted by Roberto Sebastiani. Every commercial use of this material is strictly forbidden by the copyright laws without the authorization of the authors. No copy of these slides can be displayed in public without containing this copyright notice.

Sunday, May 26, 2013

LTL Model Checking - The Automata Approach

Let $M$ be a Kripke model, and $\psi$ be an LTL formula. The model checking problem is whether $$M \models \psi$$

It is rephrased in the manner of Büchi automaton for automatic reasoning. We express both the model and the formula in Büchi automata ($A_M$, $A_\psi$), then the model checking problem is to check whether the language of $A_M$ is contained by the language of $A_\psi$, that is, $\mathcal{L}(A_M) \subseteq \mathcal{L}(A_{\psi})$. In other words, whatever $A_M$ expresses is well captured in $A_\psi$. Further, if we negate $\psi$, then the containment becomes emptiness checking. i.e. $$\mathcal{L}(A_M) \cap \mathcal{L}(A_{\neg\psi}) = \varnothing$$

Büchi Automata

Unlike NFA/DFAs, Büchi automata have infinite words (aka. $\omega$-words). The "final" states are a set of accepting states, where a loop exists. A run on automata is an infinite execution of automaton, e.g., say the alphabet is $\Sigma = \{a,b\}$, $F=\{b\}$, a legal run can be $\rho = abbbbbb\cdots$.

Like NFA, Non-deterministic Büchi automata (NBA) have transition relations $\delta : Q \rightarrow Q $ as partial ($Q$ is the set of states), while the deterministic one total. But the subset construction from NFA to DFA doesn't apply here.

Compute $A_M$

Given a Kripke model $M$, we add an initial state, and move labels from states to incoming edges, every state becomes an accepting state. The fair version is to change the accepting states only to fair states.

Labelled Generalized Büchi Automata

We need to move the labels of Büchi Automata into states. LGBA features a set of fair conditions $FT = \{F_1, ..., F_k \}$, an accepting run must concord with all fair conditions. Formally, $$\forall i . \mathsf{inf}(\rho) \cap F_i \neq \varnothing$$ where $\mathsf{inf}$ calculates the accepting states of the run $\rho$, $F_i \subseteq Q$. Further, an LGBA has a set of initial states rather than only one in BA.

Translate LTL formulas into LGBA

This part is relatively big and it will be introduced in another post.

Synchronous Product of NBAs

Compared to synchronous product of NFAs, NBAs' product employs a tag $(1,2)$ specifying on which NBA it is running. The synchronous product is used to calculate the language intersection, $$\mathcal{L}(A_1 \times A_2) = \mathcal{L} (A_1) \cap \mathcal{L} (A_2)$$

Initial state of the product, $I = I_1 \times I_2 \times \{ 1 \}$, accepting states $F = F_1 \times Q_2 \times \{ 1 \}$, transition relations are defined such that a run on track 1 ends at one of its accepting states $F_1$, then moves on to track 2 until meeting some state in $F_2$, then it switches back. The product has such initial states and finite states to ensure that an infinite run of the product automaton must infinitely run on both $A_1$ and $A_2$.

Complement Büchi automata

The complementation involves conversion to Rabin automaton. This is to construct $A_{\neg\phi}$.

Emptiness Checking - Double nested DFS algorithm

The problem can be addressed as searching an accepting cycle reachable from an initial state. Double nested DFS algorithm employs two Hash tables, two stacks and two nested DFS routines. The following is routine 1,

DFS1(NBA A) {
  stack S1=I; stack S2=∅;
  Hashtable T1=I; Hashtable T2=∅;
  while (S1!=∅) {
    v=top(S1);
    if ∃w s.t. w∈ δ(v) && T1(w)==0 {
      hash(w,T1);
      push(w,S1);
    } else {
      pop(S1);
      if v∈F DFS2(v,S2,T2,A);
    }
  }
  return EMPTY;
}

The following is routine 2,

DFS2(state f, stack S, Hashtable T, NBA A) {
  hash(f,T);
  push(f,S);
  while (S!=∅) {
    v=top(S);
    if f∈ δ(v) return NOT_EMPTY;
    if ∃w s.t. w∈ δ(v) && T(w)==0 {
      hash(w);
      push(w);
    } else pop(S);
  }
}

DFS1 starts with the initial state, hashes each state on the path when visiting it for the first time. It invokes DFS2 when no more moves are possible and the top of stack is an accepting state. DFS2 tries to search a loop starting from this accepting state and going back to itself. When such a loop is found, it means $A$ is not empty, and the path is a combination of stack 1 and stack 2.

References

  1. R. Sebastiani, Automata-theoretic LTL Model Checking, slides on Formal Methods, 2012

Appendix

The following is a copy of original copyright notice of slides which this article is quoting.

Copyright notice: some material (text, figures) displayed in these slides is courtesy of M. Benerecetti, A. Cimatti, P. Pandya, M. Pistore, M. Roveri, and S.Tonetta, who detain its copyright. Some exampes displayed in these slides are taken from [Clarke, Grunberg & Peled, “Model Checking”, MIT Press], and their copyright is detained by the authors. All the other material is copyrighted by Roberto Sebastiani. Every commercial use of this material is strictly forbidden by the copyright laws without the authorization of the authors. No copy of these slides can be displayed in public without containing this copyright notice.

Friday, May 24, 2013

Install terminal and gcc on Android

Always read instructions carefully.

- #1 note on a survival manual, Yann Martel Life of Pi

On Android, everything is an app.

- mzt

Shell for Android is an app too. Install Terminal IDE (210MB) from the app store. Yes, this is not built-in, not default, also with limited use: vi, javac, gcc, git, ssh etc. It runs without root permission. After the installation, switch on its ugly but complete keyboard to get the full function use.

Install gcc

Under Terminal IDE, gcc is paralleled by terminal-gcc, which is not installed by default (due to the volume of gcc). If you go to help file from its main menu, you will see a series of tutorials explaining how to start making the best use of it. Here I just quote the part on gcc. On any of its terminal window (there are 4),

# cat `which install_gcc`
# install_gcc

After installation, use the following command to compile,

# terminal-gcc foo.c -o foo.o

Thursday, May 23, 2013

Bounded Model Checking Encoding

See appendix for credits.

Bounded Model Checking (BMC) is a SAT-based technique, distinguished from symbolic model checking. It converts model checking problem into satisfiability problem. BMC tends to look for counter-examples by progressively increasing an integer bound, which is the number of steps in a path. Yes, once you verified there are no counter-examples within the bound $k$, it doesn't prove $M \models f$ at all. BMC is useful in troubleshooting, to capture the flaws in the model design.

The bridge

Given a Kripke model $M$, a LTL formula $f$ and a bound $k$,

$M \models_k \mathbf{E}f$ iff ⟦$M$,$f$⟧$_k$ is satisfiable.

$\models_k$ means the property is verified in the path of $k$ steps. ⟦$M$,$f$⟧$_k$ is defined as follows,

Fig. 1 The encoding of ⟦$M$,$f$⟧$_k$ in BMC

(1) divides the denotion into the model part (2) and the property part (3). (2) shows the execution of $M$ in $k$ steps, by providing the initial state ($s_0$ is a vector of boolean variables that are assigned in such state) and transition relations of each step. (3) also consists of two portions that disjunct. The first portion says there are no loops at $s_k$ to all former states (negation of transition relation from $s_k$ to $s_{k-1}$,..., $s_0$). The second one is with loops.

Fig. 2 The paths with and without loop

We do need to separate the encodings (i.e. ⟦$f$⟧$^i_k$, $_l$⟦$f$⟧$^i_k$). For instance, only the finite path carrying a loop can verify the properties like $\mathbf{G}p$. We need to describe properties in different manner according to the existence of a loop. Here is the formal chart,

Fig. 3 ⟦$f$⟧$^i_k$ and $_l$⟦$f$⟧$^i_k$ unfolded alongside their LTL correspondence

The above is a recursive definition. The indices $i$, $k$, $l$ say respectively the current state, the integer bound, the loop point (there is an edge from $s_k$ back to $s_l$). The base case $p$, an atom, matches $p_i$ which is the assignment of $p$ at the state $s_i$. The negation is thereby defined. The loop doesn't matter for these two since we only consider an atom in the current state. The disjunction and conjunction are defined recursively. Before going further, we shall see this figure,

Fig. 4 The loop case

$\mathbf{X}g$ parallels a conditional branch definition. In the loop-less case, when $i < k$, the current state is before the bound state, then there is a next state for $s_i$. Otherwise false. Similar in the loop case, but when $i = k$, since there is a loop from $s_k$ to $s_l$, the next state exists. Think there is no $i > k$, when it loops back, $k+1$ becomes $l$, so everything is still within the bound $k$.

$\mathbf{G}g$ is simply false in the loop-less case, always UNSAT. If there is a loop, we need to make sure every state (hence as a big conjunction) with in the loop verifies $g$ and also the relays from the current state $s_i$ to the loop point $s_l$ in case of $i < l$.

$\mathbf{F}g$ is straight-forward, regarding the fact that we'd like at least one $g$ on such path (both loop-less and with loop), so a big disjunction is used.

Recall that $h \mathbf{U} g$ means $h$ remains true till $g$ becomes true. So in the loop-less case, it compares to the disjunction (satisfiable at least one of the components is true) of all possible captures, e.g., $g_i$, $h_ig_{i+1}$, $h_ih_{i+1}g_{i+2}$, ..., etc. Similar for $h \mathbf{R} g$, which says the advent of the truth of $h$ releases $g$ from being always true. That said, $g$ wasn't free (being true always) before $h$ gets its truth.

The situation becomes much more complex in the loop case for these two. If $i < l$, then it gets the part similar to the loop-less one, $$ \bigvee_{j=i}^k \bigg( {}_l\llbracket \; g \; \lrbracket_k^j \wedge \bigwedge_{n=i}^{j-1} {}_l \llbracket \; h \; \lrbracket ^n_k \bigg)$$ It is accompanied by the case that $i > l$, the idea is the property shall be verified from $s_i$ to $s_k$, then from $s_l$ to $s_{i-1}$ since there is loop $(s_k, s_l)$. So we have, $$ \bigvee_{j=l}^{i-1} \bigg( {}_l\llbracket \; g \; \lrbracket_k^j \wedge \bigwedge_{n=i}^{k} {}_l \llbracket \; h \; \lrbracket ^n_k \wedge \bigwedge_{n=l}^{j-1} {}_l\llbracket \; h \; \lrbracket_k^n \bigg)$$

The last one can be accordingly rendered.

References

  • R. Sebastiani, SAT-based Bounded Model Checking, slides on Formal Methods, 2012, link
  • A. Biere et al, Bounded Model Checking, Vol. 58, Advances in Computers, 2003, pdf

Appendix

The following is a copy of original copyright notice of slides where the images here were taken.

Copyright notice: some material (text, figures) displayed in these slides is courtesy of M. Benerecetti, A. Cimatti, P. Pandya, M. Pistore, M. Roveri, and S.Tonetta, who detain its copyright. Some exampes displayed in these slides are taken from [Clarke, Grunberg & Peled, “Model Checking”, MIT Press], and their copyright is detained by the authors. All the other material is copyrighted by Roberto Sebastiani. Every commercial use of this material is strictly forbidden by the copyright laws without the authorization of the authors. No copy of these slides can be displayed in public without containing this copyright notice.

Tuesday, May 21, 2013

Conflict-Driven Backtracking and Clause-Learning

See appendix for credits.

Conflict-Driven backtracking is a huge advancement to the classical chronological backtracking applied to the DPLL algorithm. It solves the Boolean formulas with about $10^7$ variables.

State of the art

The idea was to learn from error. When we see a conflict, we find the cause (building a conflict set), and we go back to the decision point where we could do it differently if we have had known this conflict set. It seems hard to catch for a machine. However, it is operable through the following algorithm. This is the most advanced modern approach in many SAT solvers.

Deciphering the myth

Data structure: stack partitioned into decision levels. Each level comprises of a decision literal and its implied literals (unit-propagated). Every implied literal is tagged with the clause causing its unit propagation (aka. antecedent clause).

One level in the stack can be depicted by an implication graph, where there are nodes and edges. A node without edges means a decision literal , because an edge is are marked with the antecedent clause of the literal. E.g.,

Fig. 1 An Implication Graph (Shown on Right)

Building the conflict set

It has two steps,

1. C := conflicting clause
2. repeat {
      C <- resolve C with the antecedent clause of the last
      unit-propagated literal in C
}
until { C verifies some termination criteria }

Well, we wonder what this "resolve" mean, it is a disjunction but removing $A_i \vee \neg A_i$ since they become true. Resolution is a rule saying two input clauses entails the output clause (aka. resolvent). For a detailed discussion, see Resolution (logic). By performing this, the unit propagation is undone. What about some termination criteria? Here comes the magic.

1st UIP

It means First Unique Implication Point, this is the state-of-the-art strategy. It is the first point where we find only one literal of current decision level in C. For instance (built from the same example above),

Fig. 2 Conflict set construction

Upon this, we build the conflict set: $\{ \neg A_{10} , \neg A_{11} , A_4 \}$, and "learn" (add) a new clause $c_{10} := A_{10} ∨ A_{11} ∨ \neg A_4$. Now that we reached the conflict, also we know these $\neg A_{10}$, $\neg A_{11}$ can not survive with $A_4$, so we backtrack to $\neg A_{11}$, and right there we assign $\neg A_4$. Yes, we cut off all paths to $A_4$ from that point on. We would never fall into this conflict set again (we learned from the error).

Drawbacks and a solution

We saved all these learned clauses, on a larger scale ($10^7+$), we can reach an exhaustion of space. The solution is to keep only the active ones, i.e. the ones showed up (on the edges of implication graph) in the current decision level.

Fig. 3 The breath-taking jump


Appendix

The following is a copy of original copyright notice of slides where the images here were taken.

Copyright notice: some material (text, figures) displayed in these slides is courtesy of M. Benerecetti, A. Cimatti, P. Pandya, M. Pistore, M. Roveri, and S.Tonetta, who detain its copyright. Some exampes displayed in these slides are taken from [Clarke, Grunberg & Peled, “Model Checking”, MIT Press], and their copyright is detained by the authors. All the other material is copyrighted by Roberto Sebastiani. Every commercial use of this material is strictly forbidden by the copyright laws without the authorization of the authors. No copy of these slides can be displayed in public without containing this copyright notice.

Monday, May 20, 2013

Classical Chronological Backtracking

See appendix for credits.

Chronological backtracking is an improvement for the DPLL algorithm backtracking. It can provide multiple jumps back to the assignment tree, while DPLL when there is a conflict, it simply flips the last assigned literal (thus one step).

The idea

There are two types of assignment, one is binary decision, the other is unit propagation, which is implied by the decisions. So when we reach a conflict, we jump back to the binary decision point, omitting all the implied assignment caused by that decision.

Implementation

Assignments are stored in a stack with tags: unit, open, closed. They respectively mean unit-propagation, first try (chances are still there, thus open), second try (no more chances on this literal). When a conflict is met, we pop the stack till the most recent open assignment and toggle it into closed, and continues the search.

Example

The background is a CNF SAT problem. The presented is part of its assignment tree. Red literals are already assigned. We make a binary decision (true) on $A_1$, leading the clauses $c_7$, $c_8$ be satisfied.

Fig. 1

As a consequence, $A_2, A_3, A_4, A_5, A_6$ are unit-propagated in order. But then $c_6$ would be false, reaching a conflict. Hence due to chronological backtracking idea, we remove all these new assignments since $A_1$, and push $\neg A_1$ to the stack.

Fig. 2


Appendix

The following is a copy of original copyright notice of slides where the images here were taken.

Copyright notice: some material (text, figures) displayed in these slides is courtesy of M. Benerecetti, A. Cimatti, P. Pandya, M. Pistore, M. Roveri, and S.Tonetta, who detain its copyright. Some exampes displayed in these slides are taken from [Clarke, Grunberg & Peled, “Model Checking”, MIT Press], and their copyright is detained by the authors. All the other material is copyrighted by Roberto Sebastiani. Every commercial use of this material is strictly forbidden by the copyright laws without the authorization of the authors. No copy of these slides can be displayed in public without containing this copyright notice.

Sunday, May 19, 2013

Tube view on Web Backgrounding

A single color is the simplest choice, but choosing a color is not simple. Pure white background or black might be mediocre. It can't be too bright, because it is subsidiary as the name indicates.

Not So White

If we go to ubuntu.com, press ctrl+shift+I (Chrome), navigate to body tag, here it might be

background: #fff url("/sites/ubuntu/latest/u/img/patterns/body_bg.jpg");

If you examine clearly (tilt your screen), body_bg.jpg is not a pure white image, otherwise it would be here. Yep, it is a seamless background image with patterns on it.

credit: ubuntu.com

Under Ubuntu, one may turn to GIMP for such mission (link). An excerpt is to use Filters > Map > Make Seamless, you can test it under Filters > Map > Tile in a bigger canvas (e.g., double-sized). Remind that the seamless background images come in squares so that they can be easily tiled.

Stripes

credit: ibelieveinadv.com

A 1px stripe is not alluring, but the arrangement of many of them might. See this website for instance (link), it uses

background: #2f2f2f url("http://www.ibelieveinadv.com/commons/stripes.gif");

By default, a background-image is repeated (tiled) both vertically and horizontally.

When backgrounds become content

Indeed, the role of images of large resolution seems blurred, but the effect won't. See worldwildlife.org (link), but the technologies behind should be applied too (Large Images in Rails). A full-size illustration may make your site cuter (link).

More is to come...

Wednesday, May 15, 2013

Anatomy of A Periodic Program

The program body is here,

http://disi.unitn.it/~abeni/RTOS/periodic-1.c

First to mention that a periodic program is that it is activated periodically, i.e. the program wakes up periodically (it is ready for execution). Under Linux kernel, you could trace such wake up events (sched_wake_up) through ftrace. The sample program uses a real-time timer ITIMER_REAL to create periodic interrupts. The timer is set initially 2000000 us (=2s) and thence 5000us (5ms).

start_periodic_timer(2000000, 5000);

In further detail, that is

signal(SIGALRM, sighand);

Notice that sighand is the name of the call-back function. Whenever there a SIGALRM fires within the program, the function sighand is called. Though in the example it is a do-nothing function. The signal function registers sighand as the call-back, but it doesn't execute it.

The following does the job to set periods and the first round offset (this is to ensure the periodicity since we are still initializing the timer before the real periodic part comes). The timer ITIMER_REAL fires the signal SIGALRM when the timer count decreases to zero (expires), as a consequence, signal goes executed.

setitimer(ITIMER_REAL, &t, NULL);

So there are periodic interrupts on which a futile function is run (whence the program wakes up). The following infinite loop does sleeping till the signal is fired (pause()), then an in-genuine job_body() is under way. The job body function is "controlled" within 5ms such that all interrupt signals are captured on-time.

    while(1) {
        wait_next_activation();
        job_body();
    }

Conclusion

An implementation of periodic programs follows this pattern,

void *PeriodicTask(void *arg)
{
    <initialization>;
    <start periodic timer, period = T>;
    while (cond) {
        <read sensors>;
        <update outputs>;
        <update state variables>;
        <wait next activation>;
    }
}

Thursday, May 9, 2013

Region Automata and Zone Automata

As a sequel of a previous article on timed automaton (link), here we introduce its computational models.

1. Region

Why region automata? Timed automata have infinite state space (time be divided into infinite pieces), region automata give a finite partition of timed automata such that the computation becomes possible.

Intuition A region is a set of equivalent states. The partition divides the state space into different equivalent classes (regions).

Temporal constraint given by this grammar $\phi := x > c | x < c | x = c | \phi \wedge \phi$, $c$ must be an integer constant (to ensure non-zenoness)

Equivalent class The set of states which satisfies the same set of temporal constraints.

Region equivalence states are equivalent due to being in the same region, they are either within the integer grid, on the $x=c$ or $y=c$ axes, or above/below the diagonal of the integer grid. (see Figure 1.)

Fig 1. Regions as equivalent classes

Remind that largest constant relevant $c$ is actually the ceiling of $x_i$, i.e. $c = \lceil x_i \rceil$. Figure 2 is an example of partitions (regions) of the state space of a timed automaton. Not only are those shadowed areas regions, but also segments of lines (they usually are a result of clock resetting).

Fig 2. Regions on a 2-clock timed automaton

A further example Figure 3 shows the region representation of a simple timed automaton. Location $F$ is shadowed since it may loop forever, a bad design (livelock).

Fig 3. Timed automaton represented in regions

Time-abstract bisimulation If $w \simeq v$, $w,v \in l$, 1) after action $a$, $w'$ is in the region of location $l'$, so is $v'$; 2) $\forall d \exists d' . w+d \simeq v+d'$. They are respectively the transition on action and the transition on delay.

Region equivalence relation is a time-abstract bisimulation ($\simeq$).

Region reset The clock for all equivalent states is reset, hence the operation projects the whole region onto the clock axis (i.e. a line of shadow).

2. Zone

Why zone automata? Regions are still too many, we can force them collapse into unions of regions, where the unions are convex, i.e. no angles are larger than 180 degrees.

Zone Zones are so-called symbolic state (conjunction of regions). Formally, $Z = (s, \varphi)$, that is to start from a location (state) $s$ in a timed automaton, we make a conjunction of regions specified by temporal constraint $\varphi$.

Zone automaton A transition system for zones. Formally, $Z = (Q, Q^0, \Sigma, R)$, set of zones, initial zone, set of transition labels, transition relation.

Symbolic transition It may involve operations such as intersection (conjuncts), delay (stretches diagonally as x,y propagate in time simultaneously), reset (projects a shadow on the time axis). For a zone $Z = (s, \varphi)$, the transition is denoted as $\mathsf{succ}(\varphi, e)$, where $e$ is the label of switch. When $e$ is executed, $Z$ propagates by time till the time constraint $\varphi$ is met. The action is thus invoked. Proceed with a reset if it is needed.

Fig 4. Transitions on Zone Automaton

Figure 4 showed a symbolic transition from location n to m, i.e. $(n, 1 \leqslant x \leqslant 4, 1 \leqslant y \leqslant 3) \rightarrow (m, x>3,y=0)$

References

  1. R. Sebastiani, Timed and Hybrid Systems: Formal Modeling and Verification, slides of Formal Methods course, 2012, link

Appendix

The most of this post is heavily extracted from the RS's teaching slides, hence I don't claim the copyright. The character of this post is intended to be a note, with marginal and personal remarks. For those who need to respect the source, please refer the link in the references.

Wednesday, May 8, 2013

A Glimpse of Timed Automata

Terms

Timed Automaton Intuitively, an automaton with clocks, the transitions from state to state are constrained by time. Formally, $A = (L, L^0, \Sigma, X, I, E)$, respectively the set of locations (states), the set of initial locations, labels, clocks, invariants, the set of edges (transitions) $$E = \{ (s, a, \varphi, \lambda, s') | s,s' \in L, a \in \Sigma, \varphi \text{:clock constraints}, \lambda \subseteq X \}$$

Clock a stopwatch in this context, i.e. clocks are to measure the elapsed time, it can be reset.

Guard Boolean comparison between the clock and some integer value, serves as a constraint for the switch from one location to another

Action the label of transition, used to synchronize actions among several timed automata

Reset set the clock to time 0 and meanwhile the clock starts ticking again

Invariant a time constraint residing inside the state which must be respected when staying within such state, otherwise, it must move out.

Deadlock cases are, there are no more allowed moves (due to bad design of automata).

Example

We quote an automaton from this slide [1],

Figure 1. An Example Timed Automaton

  • $s_i$'s are state labels
  • two clocks present $x$, $y$
  • after action $a$, it can only stay in $s_1$ for no more than $1$ time unit
  • action $d$ can occur only when clock $y$ reads more than $2$ (due to the guard $y>2$)

References

  1. R. Sebastiani, Timed and Hybrid Systems: Formal Modeling and Verification, slides of Formal Methods course, 2012

Sunday, May 5, 2013

Life of Me

So it comes to this moment that I shall write what a true blogger practices. Not those lifeless pieces of knowledge, not wild copies of diffused computer techniques, or minute excerpts or backup discoveries. After all, after hunting after the ocean of webpages to obtain a very portion of nutrition, one wonders about the behind scenes and how the world bloggers think. Simply, a real person to talk with, on the somewhat crossed paths, or even colleagues of the same kind. You know, the laws of attraction.

The prime purpose of this blog was nothing but put aside some tricks that I came across so that later on I can easily find them. So why this turn? Why didn't I write these lines from the very beginning?

Well, I tried, in my second mother tongue. I was a pride self-assumed writer. I have jotted down many of my own guts, most of them obscure and in an archaic style so that no one except those who know me well could bother reading. My journalist-to-be brother definitely attempted to seek a way to understand me, being elder made him fraternal and faster-matured. We had a geographic segregation since every of us had departed to different universities, his in northwest and mine northeast. The span was the width of China. My mother tongue is a Long dialect. And I quickly mastered Mandarin with the spicy of northeastern accent while I stayed four years in the college. I admit that I have quite a talent of mimicking sounds, but not so much on memory. I was terrified to force myself to remember at grade two. We were asked to recite a short paragraph, only three lines. I had fought so hard but I could not manage. Nonetheless, I grew up, with a rather noteworthy fame at the place. During my university period, I observed and struggled, sought and sighed, alone. We met a few times, each time ended up arguing until both were tired. There was a lack of perception. We are seemingly divided by fate. It lasted until today and I have moved to Europe while he becomes a real news reporter. We haven't talked in depth, only some family greetings. There have not been acknowledgeable comments of my writings. My perplexed groaning was like a grain dropped into a pond. Until one day I was provoked to take off everything from my first blog. The blog host set one post as hidden. I thus wrote a python snippet to scrape out my fruits. My major is Informatics, not to brag. To write a piece of running code you need aches as the same when I construe the very picture in my head and put them into readable words. They do take time more than you could plan. I am still on this steep rising learning curve. I had a plea to terminate the amateur author life. Being in a prestigious European university and studying science you could just accord that writing is too much a luxurious leisure. The reality smashed in my face saying nothing is necessary but survival. Music is just in the background to sooth you in hardship. Parties belong to the drinking dudes. News is all of a manipulation of public thought. Religion, a salvation when you have lost your secular hope and become desperate. Talent for languages in such a multilingual context, a not-so-relevant skill to have for decoding the mystery of mathematics, to mention, Computability and Computational Complexity etc. To speak of truth, right now I am into this far-reaching nearby leisure again. Then why?

To solve this, I need to tell more of my latest deviation from the thesis work. I have taken my liberty to taste the whole of Yann's Life of Pi, so the Ang Lee's film. Shall we put this page down at our feet, and scream we are back?! We will see. I had meant to write a comment of Pi, but what do you see?

Abstraction in Model Checking

Finite Transition System $M = (S, I, R, L)$, respectively the set of states, the set of initial states, the set of transition relations, labels. Simply put, a computational model, similar to Finite State Machine.

Which Computation? Well, model checking. $M \models \varphi$

Why abstraction? Too many states to compute and the abstraction reduces the number of states.

Why abstraction works? The existential-quantified properties (ECTL) are preserved after the abstraction ($M$ simulates $M'$, i.e., $M$ has whatever $M'$ has), that is, $M' \models \varphi \rightarrow M \models \varphi$. (But not vice versa!)

Now let's go to terms.

Abstraction function $h: S \rightarrow S'$

Simulation $M$ simulates $M'$ when each transition of $M'$ has a corresponding one in $M$. The simulation is the set of pairs of states $p \subseteq \{ (s,s') | s \in S, s' \in S' \}$ that records such behavior. It is the set denotation of the abstract function $h$.

Bisimulation The simulation applies on both sides. According to property preservation, $M \models \varphi \rightarrow M' \models \varphi$. As a consequence, $M \not \models \varphi \rightarrow M' \not \models \varphi$, otherwise we reach a contradiction.

$M$ simulates $M'$, plainly put, $M$ is an abstraction (simulation) from $M'$.

What about universal-quantified properties? (in LTL or ACTL) They are preserved when $M'$ simulates $M$. That is, $$M' \models \varphi \rightarrow M \models \varphi$$ Yes, same conclusion but different condition. Still, the reverse doesn't hold.

Exercise

Credit: ~rseba, disi.unitn.it

If we draw a relation $p = \{(S_{ij}, T_i) | \text{for all possible } i,j \}$, we see (with effort) that $p$ is a simulation from $M$ to $M'$ (i.e. $M'$ simulates $M$). Verify it by the rigorous definition, if $(S_{11}, T_1) \in p$, $(S_{11}, S_{12}) \in R_M$, $\exists (T_1, T_1) \in R_{M'}$ s.t. $(S_{12}, T_1) \in p$. So are the rest transition relations of $M$. Hence, the universal-quantified property preservation applies. e.g. if $\varphi$ is pure boolean, $$M' \models \mathbf{AG} \varphi \rightarrow M \models \mathbf{AG} \varphi$$

To note that the reverse doesn't hold. For instance, $(S_{13}, T_1) \in p$, $(T_1, T_1) \in R_{M'}$, $\forall j. \nexists (S_{13},S_{1j}) \in R_{M}$ s.t. $(S_{1j},T_1) \in p$.

Saturday, May 4, 2013

Shell: Copy to Clipboard

With the help of xclip, one can copy the whole text file to the system clipboard

$ sudo apt-get install xclip

The following copys the content of foo file to clipboard (X selection)

$ cat foo | xclip -selection c

Once copied, put it into a file

xclip -o > foo

Friday, May 3, 2013

A Walk-through of A Character Device Driver

This article explains how to compile a sample Linux character device driver and how to read and write from the device.

A Sample Character Device Driver

The sample code is a copy of ldd3's example code sleepy.

/*
 * sleepy.c -- the writers awake the readers
 *
 * Copyright (C) 2001 Alessandro Rubini and Jonathan Corbet
 * Copyright (C) 2001 O'Reilly & Associates
 *
 * The source code in this file can be freely used, adapted,
 * and redistributed in source or binary form, so long as an
 * acknowledgment appears in derived source files.  The citation
 * should list that the code comes from the book "Linux Device
 * Drivers" by Alessandro Rubini and Jonathan Corbet, published
 * by O'Reilly & Associates.   No warranty is attached;
 * we cannot take responsibility for errors or fitness for use.
 *
 * $Id: sleepy.c,v 1.7 2004/09/26 07:02:43 gregkh Exp $
 */

#include <linux/module.h>
#include <linux/init.h>

#include <linux/sched.h>  /* current and everything */
#include <linux/kernel.h> /* printk() */
#include <linux/fs.h>     /* everything... */
#include <linux/types.h>  /* size_t */
#include <linux/wait.h>

MODULE_LICENSE("Dual BSD/GPL");

static int sleepy_major = 0;

static DECLARE_WAIT_QUEUE_HEAD(wq);
static int flag = 0;

ssize_t sleepy_read (struct file *filp, char __user *buf, size_t count, loff_t *pos)
{
 printk(KERN_DEBUG "process %i (%s) going to sleep\n",
   current->pid, current->comm);
 wait_event_interruptible(wq, flag != 0);
 flag = 0;
 printk(KERN_DEBUG "awoken %i (%s)\n", current->pid, current->comm);
 return 0; /* EOF */
}

ssize_t sleepy_write (struct file *filp, const char __user *buf, size_t count,
  loff_t *pos)
{
 printk(KERN_DEBUG "process %i (%s) awakening the readers...\n",
   current->pid, current->comm);
 flag = 1;
 wake_up_interruptible(&wq);
 return count; /* succeed, to avoid retrial */
}


struct file_operations sleepy_fops = {
 .owner = THIS_MODULE,
 .read =  sleepy_read,
 .write = sleepy_write,
};


int sleepy_init(void)
{
 int result;

 /*
  * Register your major, and accept a dynamic number
  */
 result = register_chrdev(sleepy_major, "sleepy", &sleepy_fops);
 if (result < 0)
  return result;
 if (sleepy_major == 0)
  sleepy_major = result; /* dynamic */
 return 0;
}

void sleepy_cleanup(void)
{
 unregister_chrdev(sleepy_major, "sleepy");
}

module_init(sleepy_init);
module_exit(sleepy_cleanup);

Makefile

obj-m = sleepy.o
KVERSION = $(shell uname -r)
PWD = $(shell pwd)
all:
	make -C /lib/modules/$(KVERSION)/build M=$(PWD) modules
clean:
	make -C /lib/modules/$(KVERSION)/build M=$(PWD) clean

Compile The Driver

The ultimate way is to compile it along with a built kernel tree. However, for the time being, installing Linux kernel headers would suffice. It should already be installed by default.

sudo apt-get install linux-headers-$(uname -r)

If installed, type

make

Load and Remove The Driver

You will see some new files are generated, including sleepy.ko, to load this module

sudo insmod sleepy.ko

To unload,

sudo rmmod sleepy

Read from and write to the device

The sleepy is created with a dynamic major, we need to create a device file for it. First get the major number,

$ cat /proc/devices | grep sleepy
250 sleepy

Then create a node under /dev, c is to create a character file, 0 is its minor number.

sudo mknod /dev/sleepy c 250 0

Now we can read and write the device using C library function read, write, or from shell

echo "sleep" > /dev/sleepy
cat /dev/sleepy

Though what sleepy does is that it makes the reader process fall asleep while the writer process wakes all readers up.

#include <fcntl.h>
#include <unistd.h>

int fd;
char buffer[32];

fd = open("/dev/sleepy", O_RDONLY);
read(fd,buffer,10);

Monday, April 22, 2013

Ubuntu: Display Tibetan Characters

To display Tibetan characters on Ubuntu/Linux, one need to install Tibetan language support. First go to Dash (press Win Key or on Mac ), search language support, click Install/Remove Lanugages button, and select Tibetan from the list, then Apply Changes.

Brightness Key Freezes Ubuntu 12.04

Notebook: Dell INSPIRON 1564. There was no such problem in Ubuntu 11.04. Don't upgrade to 12.10, you will encounter ugly interface problem (see here).

Noticed from here: askubuntu, a method was proposed, which was to modify a line in /etc/default/grub into

GRUB_CMDLINE_LINUX_DEFAULT="quiet splash acpi_backlight=vendor acpi_osi=Linux"
And then update and reboot
sudo update-grub
sudo reboot

Although I tried the same, I don't confirm this will definitely work. My experience is, if you tap slowly one at a time until it changes the brightness and show the notification, then proceed, it will be okay. If you are stuck in such freezing state, any keyboard combo can't save you out.

Reset brightness to lowest on reboot

That is what I wanted to do. Ubuntu didn't save (or the video driver) the last-time configuration of brightness. (link)

The solution, I too confirm, is to add a local script to be executed on reboot. Here is the excerpt.

sudo vi /etc/rc.local

Add the following due to your folders under /sys/class/backlight (you might need play around with it)

echo 0 > /sys/class/backlight/acpi_video0/brightness
exit 0

My machine uses a default video driver (non-proprietary) and the video card ATI RV710.

Sunday, April 21, 2013

grep Boolean Operators

OR (equivalent variations)

grep "foo\|bar"
grep -E "foo|bar"
egrep "foo|bar"
grep -e foo -e bar

AND (use grep twice)

grep foo | grep bar

NOT

grep -v foo

Sunday, April 14, 2013

An Easy Chrome App

This app is basically a link to a website.

Create manifest.json with the following content

{
  "name": "BBC News",
  "description": "BBC World News",
  "version": "1",
  "manifest_version": 2,
  "icons": { "128": "bbc-icon-128.png" },
  "app": {
    "urls":[
             "http://www.bbc.com/news"
           ],
    "launch": {
             "web_url": "http://www.bbc.com/news"
           }
  }
}

I got this icon,

At chrome://extensions/, turn on Developer Mode, and click Load unpacked extension, locate the folder, that's it!

Saturday, April 13, 2013

Get Gwibber Authorizing Twitter

Error Encountered

** Unable to load page **
** blah blah blah **
** Cannot resolve proxy hostname () **

Upgrading Gwibber From PPA

sudo add-apt-repository ppa:ubuntu-desktop/ppa
sudo apt-get update
sudo apt-get upgrade

Another personal package archive source is ppa:gwibber-daily/ppa.

Network Proxy Settings

System Settings > Network > Network Proxy > Method

Set its value none and Apply system wide.

Wednesday, April 10, 2013

Safe Ways to Force Reboot Ubuntu

(Credit: link)

If lucky,

CTRL + ALT + DEL

If still lucky, call a terminal

CTRL + ALT + F1/.../F5

If not so lucky,

ALT + SysRq (PrtScr) + K

Ah, everything fails. Here is the magic wand for Linux kernel

CTRL + ALT + SysRq (PrtScr)

That is to hold Ctrl+Alt, tap SysRq, then type in order:

REISUB

which is BUSIER in reverse order.

Reference

  1. Freezes - Linux Guide - WikiBooks
  2. Magic SysRq Key - Wikipedia

Tuesday, April 9, 2013

Rescue Windows 7

Bang!

I run into a period that I have to give up my hard disk (hardware failing).

Download OS ISO from the links provided in Windows Community (search "windows 7 home / professional iso etc.")

http://answers.microsoft.com

Burn to DVD

You know how. :) I downloaded Home Premium version (didn't find an Italian version which I was using).

Or Burn to USB!

http://wudt.codeplex.com

Windows 7 USB/DVD Download Tool is an open project from Microsoft that allows you to burn to USB easily. Try it, it is neat.

Installation

One thing needs to mention. you might see setup was unable to create a new system partition.... Windows 7 seems to find difficulty in identifying the primary drive. In this case, configure your booting priority from BIOS so that your HDD is the first. Then choose from boot options for starting from USB. Hope this helps.

Activate it

It is said to be working (confirmed now by me) if you have an OEM (most of us do) product key (on your COA label at the back, needed at installation). After installation, you will have three days to activate it. Go to Control Panel > System and Security > System, under Windows Activation, call the toll-free number shown, enter the numbers in groups, then you will receive the same amount of numbers to activate the system. It is indeed working!

Further Notes

An OEM product key is said to be reusable for the same machine. I replaced my hard disk with a new one, I think this doesn't make my notebook a new one according to Microsoft. The fact is I did have installed the English Win 7 Home Premium with my Italian Home Premium Key.

I guess Microsoft is encouraging customers to solve problems on their own so as to get rid of lots of unnecessary labor. And you are able to legally download their whole system (though not emphasized officially)!

Wednesday, April 3, 2013

awk: Filtering and Calculation

Filter wanted data columns

Here is a list of output from ftrace, filtered by the pid (12798) of sample program, then filtered with grep:

sample-12798 [003] 42655.062100: sched_stat_runtime: comm=bash pid=12798 runtime=258929 [ns] vruntime=143898862 [ns]
sample-12798 [001] 42655.062977: sched_stat_runtime: comm=sample pid=12798 runtime=864136 [ns] vruntime=94618957 [ns]
...

Print only the column of runtime,

... | awk '{printf"%s\n", substr($7,9,length($7)-8)}'

Calculate the Sum

... | awk 'BEGIN {sum=0}{sum+=$1} END {print sum}'

tikz: Plotting Functions

Use plot (in tikz package) to draw functions in $\mathrm{\LaTeX}$.

\usepackage{tikz,amsmath}

The example below generates this graph.

\begin{tikzpicture}[scale=0.5]
\draw[->] (0,0) -- (8,0) node[right] {$x$};
\draw[->] (0,0) -- (0,10) node[above] {$f(x)$};
\draw (1.5,0) -- (1.5,0.1) node[below] {$\frac{3}{2}$};
\draw (2.25,0) -- (2.25,0.1) node[below] {$\frac{5}{2}$};
\draw[dotted] (3,9) -- (3,0)  node[below] {$3$};
\draw [domain=0:3] plot (\x,{4/3 * \x*\x*\x - 8*\x*\x+15*\x}) node[right] {$\frac{4}{3}x^3-8x^2+15x$};
\draw [domain=3:6] plot (\x,{9*exp(3-\x)}) node[right] {$9e^{3-x}$};
\end{tikzpicture}

Monday, April 1, 2013

shell: Rename Multiple Files in a folder

Substitute foo in file names to bar:

for f in *;
do 
  mv $f ${f/foo/bar}
done

Prefix all .jpg files with foo and a counter:

i=1
for f in *.jpg;
do
  mv $f 'foo-'$i'.jpg'
  i=`expr $i + 1`
done

Notice spaces in expr can not be omitted.

Windows: MINGW32

You can start a MINGW32 shell command line from git cmd under Windows.

i=0;for f in *.jpg; do mv $f $i'.jpg'; i=`expr $i + 1`; done

Saturday, March 30, 2013

DOS batch: renaming multiple files with a counter

In rena.bat:
echo off
cls
set i=0
setlocal ENABLEDELAYEDEXPANSION
for /r %%x in (%1) do (
 ren "%%x" "foo-"!i!".jpg" 
 set /a i=i+1
)
The above code renames all .jpg files to be prefixed with foo and with an incrementing counter. To use the code,
rena *.jpg

Thursday, March 28, 2013

A bit of git

Install git everywhere

sudo apt-get install git

Local Directory

git init
git add .
git commit -a -m "message foo"

Prepare the server

git init

Submit to server

git remote add origin url.git
git push origin master

Further Worthwhile Reading

Sunday, March 24, 2013

C Comments: FIXME, TODO, XXX

Gedit has these comments hightlighted in yellow (credit):
/* TODO: How about auto-correcting small spelling errors? */
/* FIXME: This won't work if the file is missing. */
/* XXX: This method badly needs refactoring: should switch by core type. */

Saturday, March 23, 2013

Checking Endianness with C

The piece of code is written on April 23, 2010.
#include <stdio.h>
int checkEndian(){
 int p = 0xffff0000;
 if(*(char*)&p==0xff) //char* pointer of p's first byte
   printf("Big Endian");
 else
   printf("Little Endian"); //my pc is little endian
 return 0;
}
int main(){
   checkEndian();
}

Appendix

If the value of integer variable (32 bits) is 0xffff0000 and your system is in big endian, it will be stored as binary in memory like:
low addr:  1111 1111
       |   1111 1111
       ↓   0000 0000
high addr: 0000 0000

Friday, March 22, 2013

Users and Groups

Linux is a native multi-accessible system.

Enable and disable root

sudo password root
sudo passwd -l root
To open a shell with root, just
su

Add a new group bar

sudo groupadd bar

Add a new user foo to a group bar

sudo useradd -G bar foo

Add an existing user foo to a group bar

sudo usermod -a -G bar foo

Print current settings

id bar
groups foo