Precondition and Guard in Classic B

The differences between Precondition and Guard in B machine.

Precondition

Preconditioned substitution (termination)

• $P \mid S$ called $P$ pre $S$: PRE P THEN S END
  • The operation is only activated when P holds. Otherwise, it may result in an incorrect behaviour.
  • $[P \mid S]R \Leftrightarrow (P \land [S]R)$
  • If $P$ doesn't hold, the operation is not guaranteed to achieve anything, say $R$, since $P \land [S]R$ never holds whatever $R$. This substitution which is not able to establish anything is said to be non-terminating substitution

Guard

Guarded substitution (feasibility)

• $P \Longrightarrow S$ called $P$ guards $S$
  • $S$ is performed under the assumption $P$
  • $[ P \Longrightarrow S]R \Leftrightarrow (P \implies [S]R)$
  • If $P$ holds, post-condition $R$ is established. Otherwise, if $P$ is false, $[ P \Longrightarrow S]$ can establish anything. It's said to be non-feasible.

Differences

$P$ doesn't hold

• $P \mid S$ can not establish anything if $P$ doesn't hold. When $P$ doesn't hold, the substitution is said to abort. (Like the divergence in CSP)
• $P \Longrightarrow S$ can establish anything if $P$ doesn't hold. When $P$ doesn't hold, the substitution is not feasible.

Postcondition

• In order to establish the post-condition, $P \mid S$ must prove $P$ but $P \Longrightarrow S$ may assume $P$.

Substitution

• In $P \mid S$, $P$ is assumption, which is a contract between the user of the operations and the machine providing the operations
• In $P \Longrightarrow S$, $P$ is condition for the substitution $S$ to be feasible.
• IF P THEN S END. For example, IF 0 < n THEN n := n - 1 END is equal to if 0 < n then n := n - 1 else n := n end

Example and Demonstration

An example

    MACHINE
       PreGuardTest

    VARIABLES
        n
    INVARIANT
        n: NAT
    INITIALISATION
        n := 0
    OPERATIONS
        inc(i) = PRE
            i: NAT 
        THEN 
            n := n + i 
        END;

        dec0(d) = BEGIN
            n := n - d 
        END;

        dec(d) = PRE
            d: NAT & n >= d
        THEN 
            n := n - d 
        END;

        decp(d) = SELECT    d: NAT & n >= d THEN 
            n := n - d 
        END;

        dec1(d) = BEGIN 
            IF n >= d THEN 
                n := n - d 
            END
        END;

        dec2(d) = BEGIN 
            SELECT n > d THEN 
                n := n - d
        WHEN n = d THEN
            n := n - d
        ELSE
            n := n
            END
        END

    END

Demonstration with ProB

default PRE as SELECT

• Precondition will be treated as guard
• when n=0, call dec1(1) will cause invariant voilented.
• when n=0, dec(1) is not enabled since the precondition doesn't hold. So long as decp(1)
• when n=0, call dec1(1) won't change the value of n since the substitution n := n - d is not feasible since 0 >= 1 is false
• when n=0, dec2 works like dec1

default PRE as SELECT is false

• Precondition will be treated as precondition
• just after initialisation, ProB state window showed
  • inc(-1) will cause Precondition i: NAT violated if we assume the MININT and MAXINT is -1 and 3 separately
  • dec(-1) will cause Precondition d: NAT & n >= d violated
  • dec(1), dec(2) and dec(3) will cause Precondition d: NAT & n >= d violated as well

Proof Obligations

References

• J.-R. Abrial, The B-book: assigning programs to meanings. Cambridge University Press, 2005.
• Ken Robinson, An Introduction to the B Method Preconditions and Guards, 2001

[Latex] Math mode in Verbatim or Verb in math mode

Verb in math mode

• Include
  \usepackage{fancyvrb} % math mode in verbatim
• SaveVerb to define verb text
  \SaveVerb{verbtext}+verb text+
• UseVerb
  \UseVerb{verbtext} within math mode

Examples

\usepackage{fancyvrb} % math mode in verbatim
\SaveVerb{verbtext}+verb text+
\begin{align*}
    \UseVerb{verbtext}
\end{align*}

Color the verbatim

Define new blockcode environment

\DefineVerbatimEnvironment{blockcode}
{Verbatim}
{formatcom=\color{blue}}

Examples

\begin{blockcode}
    text to be colored
\end{blockcode}

Break lines in verb

Include this new package: spverbatim

\usepackage{spverbatim} % break lines at spaces when vs. \verb

Use \spverb

\spverb+\langle \listarg \rangle+

Examples

Math in Verbatim

• TBD

Source Code Syntax Highlight in Blogger

How to enable the source code syntax hightlighter for google blogger

SyntaxHighlighter

• Go to Blogger's template
• Click "Backup/Restore" in the upright of page to backup current template at first
• Then "Edit Template"
• Add the following lines just before the line

Examples

js

int function(int i)
{
    return i;
}

C/C++

int function(int i)
{
    return i;
}

References

• SyntaxHighlighter
• How to configure

[Latex] Cross-Reference and automatically increasing number in table cell

The below commands define two counters: cellcounter and cellcounter1, which are used for two tables seperately.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% New Command for Cross-Reference in Table cell
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcounter{cellcounter} % a new counter
% automatically increase the counter, print the value of counter, and label it for reference
\newcommand{\omegalabel}[1]{\refstepcounter{cellcounter}\arabic{cellcounter}\label{#1}}
% remember to reset before a new start
\newcommand{\cellcounterreset}{\setcounter{cellcounter}{0}} % automatically increase the counter

\newcounter{cellcounter1} % a new counter
% automatically increase the counter, print the value of counter, and label it for reference
\newcommand{\philabel}[1]{\refstepcounter{cellcounter1}\arabic{cellcounter1}\label{#1}}
% remember to reset before a new start
\newcommand{\cellcounter1reset}{\setcounter{cellcounter1}{0}} % automatically increase the counter

In the table cell, we can use it like this way.

\begin{tabular}[]{|p{0.6in}|p{1.0in}|p{1.5in}|p{3.0in}|}       
      \hline
       $\Omega_3$ Rule \omegalabel{omega3:rul_gen1} & \multicolumn{3}{p{5.5in}|}{In order to identify the state space, the initialisation and the operations, Z specification must have a schema named \I{Init} for initialisation and the only one schema included in \I{Init} schema defines the state space. A schema, which includes state schema and its decoration, and is not included by other schema, is treated as an operation.} \\ \cline{2-4}
      \hline

\end{tabular}

In another table, we can use it like this way too.

\begin{tabular}[]{|p{0.6in}|p{1.0in}|p{1.5in}|p{3.0in}|}       
        \hline
        $\Phi$ Rule \philabel{phi:rul_abbr} & $AbbrDef==exp$ & \verb+nametype AbbrDef=+ $\Phi(exp)$ & Abbreviation Definition \\
        \hline

\end{tabular}

Then, we can refer to it by

Rule~\ ref{phi:rul_abbr}
Rule~\ ref{omega3:rul_gen1}

The output will be like.

[git] usage (1)

---

Authors: - Kangfeng Ye
Title: Git Usage ...
Keywords: Git

Git Introduction

Git is a distributed version control system.

Understanding the key Terminologies

Commands

git add

• add changes in the working tree to the staging area or called staging
• allows you to incrementally modify files, stage them, modify and stage them again until you are satisfied with your changes

An example

• show current working tree status

$ git status -s

• add a new file, and edit it to add contents

$ echo "git add test" > readme.txt

• query status and it is untracked

$ git status -s
?? readme

• staging it and query status again. A - staged

$ git add readme
$ git status -s
A readme

• modify it and query status again. AM - the file has been changed but the change is not staged

$ echo "staging, then modify again" >> readme
$ git status -s
AM readme

• staging it again. It comes back to staged again.

$ git add readme; git status -s
A readme

Another example to test

• query current status

$ git status -s
A readme

• show file and it's staged content

$ cat readme
git add test
staging, then modify again

• modify it, but no staging

$ echo "no staging" >> readme
$ git status -s
AM readme

• commit it

$ git commit -m

Troubleshooting

A scenario

• create a local git repository

$cd /mnt/share/rfid_tracker
$ git init
$ touch readme.txt

• clone from repository

$cd ~/src/
$ git clone /mnt/share/rfid_tracker rfid_tracker - a clone is in rfid_tracker folder

• modify the readme.txt file and commit in clone

$ git commit -m "change" readme.txt

• push to original repository

$ git push

• an error occurs

remote: error: refusing to update checked out branch: refs/heads/master
error: failed to push some refs to /mnt/share/rfid_tracker

• solution (make original reposity as bare)

$ cd /mnt/share/rfid_tracker
$ mv .git .. && rm -fr *
$ mv ../.git .
$ mv .git/* .
$ rmdir .git
$ $ git config --bool core.bare true

How Operators: Infix, Prefix, Postfix, or Mixfix (Distfix)

How Operators: Infix, Prefix, Postfix, or Mixfix (Distfix)
Infix, prefix, postfix and Mixfix operators are different ways to write expressions equally.

Infix Notation

Operators are written in the middle of the operands

Examples

• (6-5)*7
• A*B + C/D

Prefix Notation

Also knowns as Polish notion. Operators are placed in the left of the operands

Examples

• *(- 6 5) 7 or * - 6 5 7
• + * A B / C D

Postfix Notation

Also knowns as Reverse Polish notion. Operators are placed in the right of the operands

Examples

• 6 5 - 7 *
• A B * C D / +

Outfix Notation

Operators are placed out of the operands

Examples

• |_| in Maude, e.g. | 1 0 1 1 0 | is 5

Mixfix Notation

Have several name parts and can be infix, postfix, prefix, and closed (a).

References

• Mixfix Part1
• Mixfix Part2
• Mixfix Part2a
• Mixfix parser

Examples

• if n + n == n ! then n else (n + n - n) in Agda: several name parts, mixed fixity (prefix, infix, postfix)
• L ? S : T in Maude: comination of outfix and infix

Definition

• Holes: denoted by _ in _[_]
• Precedence
• Infix _ + _: two holes and one name part +
• Prefix if _ then _ else _: three name parts (if, then, else), and three holes.

[VIM] Insert the content of a file into current opened file

read a file and insert it into the position below the cursor of the current file

:read /path/to/file

:re /path/to/file

:r /path/to/file

• insert into the beginning of the file

:0r /path/to/file

• insert into the end of the file

:$r /path/to/file

read the output of system command and insert into the position below the cursor of the current file

• read in the file list by ls command

    :r !ls
  
    :r !ls ~

• read in the dir tree by tree command

    :r !tree

read a specific lines from a file and insert it into the position below the cursor of the current file

• read the line no.10 to 20 into current file

:r !sed -n 10,20p /path/to/file

Match two marks in one line or two successive lines by grep or awk

Sometime we may need to check if a text file contains the wanted information which can be in one line or two sequential lines, but not others. For example we may check if a file contains the "operation system" and "Linux". It limits to the following format:

In one line:
        "operation system Linux" or "operation systems such as Unix, Linux, Windows..."
or
        "operation system
        Linux"
or
         "operation systems such
          as Unix, Linux, Windows... "
but not
         "Linux operation system"
not
         "Linux
          operation system"
not
         "operation system
         ......
         Linux"

pcregrep

pcregrep -M 'operation system.*(\n|.).*Linux' test.txt

awk

awk '/operation system/{k=1; ln=$0}  /Linux/{if(k == 1){print "--------"; print ;} if(k == 2){print "---------"; print ln; print;}} {if(k > 0){k++}}' test.txt

Problem: this awk will match the "Linux operation system"? How to avoid it?

Improvement: 

./match.awk test.txt

match.awk

#!/usr/bin/awk -f

BEGIN \
{
        print " - BEGIN - "
        m1 = 0; # mark1
        m2 = 0; # mark2
        ln = ""; # last line
}
{
        # two marks in one line
        if ($0 ~ /operation system.*Linux/) {
                        print "----1----";
                        print $0;
        }
        else {
                if ($0 ~ /operation system/) {
                        m1 = 1;
                        ln = $0;
                }
                else if ($0 ~ /Linux/ && m1 == 1) {
                # two marks in adjacent lines
                        m2 = 1;
                        print "----2----";
                        print ln;
                        print $0;
                }
                else {
                # clear all variables for unmatched line
                        m1 = 0;
                        m2 = 0;
                        ln = "";
                }
        }
}
END { print " - DONE - " }

Test Output

 - BEGIN -
----1----
operation system Linux
----2----
operation system
Linux
----1----
operation system such as Linux
----2----
operation system
such as Linux
 - DONE -

Test Input: test.txt

operation system Linux

operation system
Linux

operation system such as Linux

operation system
such as Linux

Linux
operation system

Linux operation system

operation system

Linux

operation system
such as
Linux

[English Writing] commas (,) usage

Basic Rules

For more, please refer to grammarbook.com

R1. Dependent clause + Main clause

When starting a sentence with a weak clause, use a comma after it. Conversely, do not use a comma when the sentence starts with a strong clause followed by a weak clause. (from grammarbook.com)

Examples:

• If I ever complete my PhD successfully, I will be amazed.
  • I will be amazed if I ever complete my PhD successfully.
• When I use it, the e-mail always breaks down.
  • The e-mail always breaks down when I use it.

R2. Adverbs that relate to the whole sentences

Examples:

• However, some researches adopt a markedly different approach.
• Superisingly, he did not go to the school yesterday.

R3. Speech + comment

Examples:

• "Paul Klee," he remarked, "was the first person to acutally paint commas".

R4. When a sentence is 'broken open' in the middle

Examples:

• Some researches, on the other hand, adopt a different approach.
• There are, it seems, two different solutions to the enthanasia problem.

R5. Items in lists

Use commas to separate words and word groups with a series of three or more.

Examples:

• Many essays are over-long, convoluted and boring. [UK]
• Many essays are over-long, convoluted, and boring. [US]
• Do not steal, copy, or plagiarise ideas.

R6. Separate two adjectives when end can be inserted between them

Examples:

• He is a strong, healthy man.
  • He is a strong and healthy man.
• He is a lonely, young boy.

R7. Separate day and month from the year when writing date.

Examples:

• I will have a business travel from May 15th, 2011.
• I will have a business travel from May 2011. (If day, month or year is ommitted, no comma)

[English Writing] hyphen and dashes

Three types of dashes and its corresponding Latex within parentheses

• Hyphen - (-)
• en dash – (--)
• em dash — (---)

Hyphen - (-)

A short horizontal mark of punctuation ( - ) used between the parts of a compound word or name or between the syllables of a word when divided at the end of a line. (from About)

Examples:

• concatenation of compount words, e.g. eight-year-old
• on-site support
• follow-up

en dash – (--)

• An en dash, roughly the width of an n, is a little longer than a hyphen. It is used for periods of time when you might otherwise use to. (from grammarbook)
• An en dash is also used in place of a hyphen when combining open compounds.
  • attaches a prefix or suffix to an unhyphenated compound

Examples:

• section 3–5
• post–World War I treaty
• New York–based writer

em dash — (---)

A mark of punctuation (—), technically known as an em dash, used to set off a word or phrase after an independent clause or to set off words, phrases, or clauses that interrupt a sentence. (from About)
"A dash is a mark of separation stronger than a comma, less formal than a colon, and more relaxed than parentheses." (William Strunk, Jr, and E.B. White, The Elements of Style)

Set Off Words or Phrases After an Independent Clause

"Life, said Samuel Butler, is like giving a concert on the violin while learning to play the instrument—that, friends, is real wisdom." (Saul Bellow, "My Paris," 1983)
"By trying we can easily learn to endure adversity—another man's, I mean." (Mark Twain)

Dashes Used to Set Off Words or Phrases That Interrupt a Sentence

Then, a review of model checking approaches—refinement based and temporal logic based—for currently applicable tools is taken, which provides the insight into the appropriate approaches for Circus and CML
"Copper Lincoln cents—pale zinc-coated steel for a year in the war—figure in my earliest impressions of money." (John Updike, "A Sense of Change." The New Yorker, Apr. 26, 1999)

Reference numbering in Latex

Problems

Multiple references may cause a very weird problem.

For example, some time this VDM [2][1] is gotten from the LaTeX \cite{vdm2001} \cite{vdm1999}.

The order in reference is not correct. The right order will not depend on which citation is placed first and it should depend on which reference is referred first.

Solution 1

Use the cite package

\usepackage{cite} \cite{vdm2001, vdm1999}

This will result in VDM [1,2]

Solution 2

Use the natbib package with options

\usepackage[sort&compress]{natbib}

• \citet for textual citations
• \citep for parenthetical citations

For example

• \citet{vdm2001}
• \citep{vdm2001}
• \citet[p.~20]{vdm2001}
• \citet[chap.~2]{vdm2001}
• \citet{vdm2001,vdm1999}

R: basics - installastion, environment and debug

Install R

• $sudo apt-get install r-base

R edit environment

• Install vim-r-plugin
• Install vim screen plugin
• Install tmux tool by "apt-get install tmux"

R basics

• Install extra package
  • > install.packages("ismev")
• Source R script
  • > source("fit-gumbel.r")
• Call function provided by fit-gumbel.r
  • > fit-gumbel("in.dat")

R debug

take optim function as an example

• display source code of optim
  • > edit(optim)
• set debug mode
  • > debug(optim)
• check debug mode
  • > isdebugged(optim)
• cancel debug mode
  • > undebug(optim)
• debug optim (R source code src/library/stats/R/optim.R)
  • > debug(optim)
  • > out <- gumbel(dat)
  • Browser[2]> where
  • Browser[2]> [RET] - next step
  • Browser[2]> c - continue
  • Browser[2]> n
  • Browser[2]> Q
  • Browser[2]>

tmux usage

• tmux quick set
  • tmux to take out the tmux terminal environment
  • C-b % to split window into two panes (vertically)
  • C-b :split-window to split window into two panes (horizontally)
  • C-b o switch to next pane
  • C-b x kill current pane
• C-b has change to C-a
  • download a tmux.conf file
  • tmux source-file /devt/dev-rye/tmux-conf/tmux.conf
  • C-a | split vertically
  • C-a - split horizontally

Author name is 3em dash when using bibtex file to output bibliography in Latex

Problems

Entry in .bib file (edit by Jabref)

@INBOOK{Baier2008a,
  chapter = {4},
  pages = {170-198},
  title = {{P}rinciples of model checking},
  publisher = {MIT Press},
  year = {2008},
  author = {Christel Baier and Joost-Pieter Katoen},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  isbn = {978-0-262-02649-9},
  owner = {randall},
  timestamp = {2013.05.23}
}

The output will be like that:

[22] ——, Principles of model checking. MIT Press, 2008, ch. 4, pp. 170–198.

Try
If I remove the hyphen which is used to connect the name, it will be alright.

@INBOOK{Baier2008a,
  chapter = {4},
  pages = {170-198},
  title = {{P}rinciples of model checking},
  publisher = {MIT Press},
  year = {2008},
  author = {Christel Baier and Joost-Pieter Katoen},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  isbn = {978-0-262-02649-9},
  owner = {randall},
  timestamp = {2013.05.23}
}

The output will be like that:

[22] C. Baier and J. P. Katoen, Principles of model checking. MIT Press, 2008,
ch. 4, pp. 170–198.

However, the similar entry 

@BOOK{Baier2008,
  title = {{P}rinciples of model checking},
  publisher = {MIT Press},
  year = {2008},
  author = {Christel Baier and Joost-Pieter Katoen},
  pages = {I-XVII, 1-975},
  bibsource = {DBLP, http://dblp.uni-trier.de},
  isbn = {978-0-262-02649-9},
  owner = {randall},
  timestamp = {2013.05.23}
}

will give the right output

[21] C. Baier and J.-P. Katoen, Principles of model checking. MIT Press, 2008.

Root Cause
If two entries in .bib file have the same author name, then one of them will become 3em dash (——).
It's default behaviour defined in IEEEtran.bst style. 


To remove this limitation, change the CTLdash_repeated_names value to no in .bib file

@IEEEtranBSTCTL{IEEEexample:BSTcontrol,
  CTLdash_repeated_names = "no"
}

Then add the following line in the tex file

\bstctlcite{IEEEexample:BSTcontrol}

However,  if the documentclass is not IEEEtrans, then this command \bstctlcite is not available. So this try will failed too.

Solution:
For the Latex file which has documentclass IEEEtrans, the above solution may be applied. For others (Article and Book class), just leave (——), it's not an error

"LaTeX Error: Too many math alphabets used in version czt"

This error means you have used more than 16 math symbol fonts (latex limitation).

Solution 1:  (http://valis.cs.uiuc.edu/blog/?cat=37)
Bypass this limit by specifying the only used font, e.g.

$\text{\usefont{U}{bbm}{m}{n}{H}}$ 

 Solution 2: (Work for this case)
 Replace the txfonts package with mathtools
Or remove the txfonts package if you don't need it

%\usepackage{txfonts} %\varparallel
 \usepackage{mathtools}

Solution 3:
too many math alphabets in version normal

\usepackage{amssymb}

\newcommand\hmmax{0} % default 3
 % \newcommand\bmmax{0} % default 4
 \usepackage{bm}

Substitution, Unification and Term Rewriting

Unification is the basis of term rewriting system, and unification algorithms is the heart of the computation model of logic programs.

Term:

terms are expressions which can be obtained from constant symbols, variables and function symbols. Constant symbols are the 0-ary functions, so no special syntactic class is needed for them.

• Function symbols: one that has no other property than its name and arity
• Terms that do not contain free variables are known as ground terms
• A ground term of a formal system is a term that does not contain any free variables;
• free variable: y is free variable in $\forall x \in X \bullet (x+y) > 0$
• bound variable: x is bound variable in $\forall x \in X \bullet (x+y) > 0$
• Hence $\forall x \in X \bullet (x+y) > 0$ is not a ground term, but $\forall x \in X \bullet x > 0$ is a ground term
• x and y are variables, and f is a binary function symbol, then $f(x,y)$ is a term

Arity - the number of arguments or operands the functions or operation accepts. For example, the arity of $f(x)=x+1$ is 1; the arity of $f = 3$ is 0; the arity of $f(x,y,z) = x + y + z$ is 3.

• 0-ary function or operation: (arity == 0) constant symbols
• unary function or operation: (arity == 1) such as $f(x) = x * 2$, (unary operator) $-x$
• binary function or operation: (arity == 2) such as $f(x,y) = x + y$
• ternary function or operation: (arity == 3)

Signature:

A signature $\Sigma$ is a set of function symbols, where each $f \in \Sigma$ is associated with a non-negative integer n, the arity of $f$. $\Sigma^{0}$ denotes a set of constant symbols, while $\Sigma^{n}$ denotes a set of n-ary function symbols.

• For example, group $\Sigma_G := \{e, i, f \}$ where e is 0-ary, i is 1-ary, and f is 2-ary
• For example, a set of non-negative integers. e for smallest non-negative integer, i denotes the successor function $succ(x) = x + 1$, and f denotes the addition function $f(x,y) = x + y$

Substitution:

Substitution is a syntactic transformation on strings of symbols of a formal language

• a substitution is a finite set of the form $$\theta =  \{v_1 \mapsto t_1, ..., v_n \mapsto t_n \}$$ , where 
• $v_i$: distinct variables; 
• $t_i$: terms with $t_i \ne v_i$;
• $v_i \mapsto t_i$: binding

• Substitution application:  $E \theta$
• E - expression
• $\theta$ - substitution
• Simultaneously replacing each occurrence of $v_i$ in E with $t_i$
• For example, $E = p(x,y,f(a))$, $\theta = \{x \mapsto b, y \mapsto x\}$, $E \theta = p(b,x,f(a))$.
  

• Substitution Composition
• Two substitutions:  $$\theta =  \{v_1 \mapsto t_1, ..., v_n \mapsto t_n \}$$ $$\sigma =  \{u_1 \mapsto s_1, ..., u_n \mapsto s_n \}$$ $$\theta \sigma =  \{v_1 \mapsto t_1 \sigma, ..., v_n \mapsto t_n \sigma,  u_1 \mapsto s_1, ..., u_n \mapsto s_n\}$$
• For example, $\theta = \{x \mapsto f(y), y \mapsto z\}$, $\sigma = \{x \mapsto a, y \mapsto b, z \mapsto y\}$, $\theta \sigma = \{x \mapsto f(b), z \mapsto y\}$

• Empty Substitution $\varepsilon$
• Renaming substitution
• $\theta =  \{x_1 \mapsto y_1, ..., x_n \mapsto y_n \}$ is a renaming substitution if $y_i$ are distinct variables

• More general substitution (MGS)
• a substitution $\theta$ is more general than a substitution $\sigma$, written $\theta \leq \sigma$, iff there exists a substitution $\lambda$ that $$\theta \lambda = \sigma$$

Abstract Reduction System:

• An abstract reduction system is a pair $(A, \to)$, where the reduction $\to$ is a binary relation on the set A, i.e. $\to \subseteq A \times A$. Written $a \to b$, instead of $(a,b) \in \to$
• Program evaluation: $a0 \to a1 \to ...$. Starting from the initial program a0, and try to reach a normal formal
• Normal formal is the program which can not be reducible
• Let $\Sigma$ be a signature and $V$ a countably infinite set of variables disjoint from $\Sigma$. A $\Sigma$-identity is a pair $(s,t) \in T(\Sigma, V) \times T(\Sigma, V)$. Identities will be written as $s \approx t$
• reduction relation $\to_E$, where E is a set of $\Sigma$-identity
  

Unification:

Unification, in computer science and logic, is an algorithmic process by which one attempts to solve the satisfiability problem. The goal of unification is to find a substitution which demonstrates that two seemingly different terms are in fact either identical or just equal. Unification is widely used in automated reasoning, logic programming and programming language type system implementation

• Unification is the process of solving the satisfiability problem: given $E$, $s$ and $t$, find a substitution $\theta$ such that $\theta s \approx_E \theta t$
• For special case, where $E=\emptyset$, this case of unification is called syntactic unification, because the unification aims to find a $\theta$ such that $\theta s = \theta t$ i.e. $\theta s$ and $\theta t$ are syntactically identical.
• If $E \neq \emptyset$, this is referred to semantic unification
• Unifier of Expressions: a substitution $\theta$ is a unifier of expressions E and F iff $$\theta E = \theta F$$
• For example, $E = f(x,b,g(z)), F = f(f(y),y,g(u))$. Then $\theta = \{x \mapsto f(b), y \mapsto b, z \mapsto u\}$ is a unifier of E and F since $$\theta E = f(f(b),b,g(u))$$ $$\theta F = f(f(b),b,g(u))$$

• Unifier is a solution to the equation by substitution. Find a substitution to make two expressions E and F are equal and this substitution is a solution to this equation, named unifier.

Unification in Prolog:

Unification in Perl:

Very good Class Diagram viewer of Java source code within Eclipse Plugin

The ObjectAid UML Explorer for Eclipse

For Class Diagram, it's free to use. But for sequence diagram, it is licensed. Please refer to http://www.objectaid.com/products.

Installation and Tutorial

• Installation
• Class Diagram 
• Sequence Diagram 

Launch czt-ide from the Eclipse and Create a new project

1. After successful import and build of CZT in Ubuntu, we can launch the czt ide from the Eclipse.

• Select the "net.sourceforge.czt.eclipse.repository" project, and right click the czt-ide.launch file, select the "Run As -> czt-ide"
• An error about "-XstartOnFirstThread" is not a recognized option for java
• Just open the Run configuration edit dialog and delete this option in the "Arguments -> VM Arguments"
• Then launch again. Succeed.

2. Create a new project circus2bcsp

• Create a new "Java Project" from the Eclipse
• Input the name "Main" and Package "net.sourceforge.czt.circus2bcsp"
• Copy the content of Main.java in z2b project and paste to Main.java in this project
• There's some errors such as "import  net.sourceforge.czt.session.Filesource can be resolved"
• Open the project properties of circus2bcsp, and go to the Project tab of Java Build Path, add the necessary projects to build together.
• Then the error will be disappeared

Enable SSH X11Forwarding to access Ubuntu from the local Mac OS X

X11Forwarding config in ssh can enable the remote desktop access from the local client. This is a set up of access between Ubuntu server and local Mac Client.

1. Ubuntu Server

• make sure the X11Forwarding option in /etc/ssh/sshd_config is set to yes. If not, set it to yes, and restart the sshd service by "sudo service ssh restart"
• test X11Forwarding in server
• Open a terminal in Ubuntu, and "ssh -v -X localhost" to establish the ssh connection with X11Forwarding. 
• Check if there's a line with "Requesting X11 Forward" shown in the debug output
• Check DISPLAY environment variables by "echo $DISPLAY" and it should be localhost:10.0

2. Mac OS X client
Reference: http://ruepprich.wordpress.com/2013/01/08/x11-forwarding-on-os-x-10-8-2-mountain-lion/

•  Install  XQuarz for Mac OS
• Open iTerm and add remote server to access list by "sudo xhost + 192.168.56.101"
• There's an error about 'xhost: unable to open display ""' 
• And ssh -X user@192.168.56.101 also failed to take X running

• Open XQuarz, and open "Terminal" in Application Menu
• bash-3.2$ xhost + 192.168.56.101
  192.168.56.101 being added to access control list
• bash-3.2$ ssh -X rye@192.168.56.101
• rye@rye-desktop:~$ echo $DISPLAY
  localhost:11.0
• xclock works

Set up Java Development Environment for CZT (Community Z Tool) On Windows

Set up Java Development Environment for CZT (Community Z Tool) On Windows

---

Windows

Install JDK-1.7.0

1. Install Directory
   
   • c:\Program Files\Java\jdk1.7.0_03
   • c:\Program Files\Java\jre7
2. Set environment variables
   
   • Path=c:\Program Files\Java\jdk1.7.0_03\bin\;c:\Program Files\Java\jre7\bin\;
   • JAVA_HOME=c:\Program Files\Java\jre7\

Install maven-3.0.5 (>= 3.0.4)

1. Download maven for Windows from http://maven.apache.org/download.cgi
2. Unpack the tar package under d:\programs
3. Add maven bin to environment variable PATH
   
   • PATH=d:\randall\Programs\apache-maven-3.0.5\bin\

Git clone czt code

    git clone git://git.code.sf.net/p/czt/code czt_code

Build CZT

• Execute buildall.bat

Build Error

1. Compilation Error #1
   

   ------- Error Log ------
   [INFO] -------------------------------------------------------------  
   [ERROR] COMPILATION ERROR :  
   [INFO] -------------------------------------------------------------  
   [ERROR] Unable to locate the Javac Compiler in:  
   c:\Program Files\Java\jre7\..\lib\tools.jar  
   Please ensure you are using JDK 1.4 or above and  
   not a JRE (the com.sun.tools.javac.Main class is required).  
   In most cases you can change the location of your Java  
   installation by setting the JAVA_HOME environment variable.  
   [INFO] 1 error  
   [INFO] -------------------------------------------------------------
   

   Solution: change JAVA_HOME to c:\Program Files\Java\jdk1.7.0_03\
2. Build failed
   Line breaks (Windows only)
   On Windows, CZT expects Windows-style line breaks (CR+LF). The conversion is usually set by default (e.g. using msysgit) and nothing else is necessary. If, however, you encounter build problems with some CZT modules, try forcing the Windows line breaks using the following Git command in your repository:
   

   git config core.autocrlf true
   

   Then reset your Git repository to checkout correct line breaks:
   

   git rm --cached -r .
   git reset --hard
   

3. Build Error

    [INFO] ------------------------------------------------------------------------
    [INFO] BUILD SUCCESS
    [INFO] ------------------------------------------------------------------------
    [INFO] Total time: 7:23.874s
    [INFO] Finished at: Tue Apr 23 10:45:24 BST 2013
    [INFO] Final Memory: 291M/784M
    [INFO] ------------------------------------------------------------------------
    [INFO] Scanning for projects...
    [WARNING] Error initializing: org.eclipse.tycho.p2.resolver.P2TargetPlatformReso lver@646d5273
    java.lang.RuntimeException: java.lang.IllegalStateException: Service is not regi
    stered class='interface org.eclipse.tycho.core.facade.ProxyServiceFacade'
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.che
    ckStarted(DefaultEquinoxEmbedder.java:301)
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.get
    Service(DefaultEquinoxEmbedder.java:275)
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.get
    Service(DefaultEquinoxEmbedder.java:270)
            at org.eclipse.tycho.p2.resolver.P2TargetPlatformResolver.initialize(P2T
    argetPlatformResolver.java:433)
            at org.sonatype.guice.plexus.lifecycles.PlexusLifecycleManager.initializ
    e(PlexusLifecycleManager.java:338)
            at org.sonatype.guice.plexus.lifecycles.PlexusLifecycleManager.manageLif
    ecycle(PlexusLifecycleManager.java:296)
            at org.sonatype.guice.plexus.lifecycles.PlexusLifecycleManager.onProvisi
    on(PlexusLifecycleManager.java:148)
            at com.google.inject.internal.ProvisionListenerStackCallback$Provision.p
    rovision(ProvisionListenerStackCallback.java:108)
            at com.google.inject.internal.ProvisionListenerStackCallback.provision(P
    rovisionListenerStackCallback.java:55)
            at com.google.inject.internal.ProviderInternalFactory.circularGet(Provid
    erInternalFactory.java:68)
            at com.google.inject.internal.InternalFactoryToInitializableAdapter.get(
    InternalFactoryToInitializableAdapter.java:45)
            at com.google.inject.internal.InjectorImpl$3$1.call(InjectorImpl.java:96
    5)
            at com.google.inject.internal.InjectorImpl.callInContext(InjectorImpl.ja
    va:1011)
            at com.google.inject.internal.InjectorImpl$3.get(InjectorImpl.java:961)
            at com.google.inject.Scopes$1$1.get(Scopes.java:59)
            at org.sonatype.guice.bean.locators.LazyBeanEntry.getValue(LazyBeanEntry
    .java:83)
            at org.sonatype.guice.plexus.locators.LazyPlexusBean.getValue(LazyPlexus
    Bean.java:49)
            at org.codehaus.plexus.DefaultPlexusContainer.lookup(DefaultPlexusContai
    ner.java:253)
            at org.codehaus.plexus.DefaultPlexusContainer.lookup(DefaultPlexusContai
    ner.java:245)
            at org.eclipse.tycho.core.resolver.DefaultTargetPlatformResolverFactory.
    lookupPlatformResolver(DefaultTargetPlatformResolverFactory.java:74)
            at org.eclipse.tycho.core.resolver.DefaultTychoDependencyResolver.setupP
    roject(DefaultTychoDependencyResolver.java:86)
            at org.eclipse.tycho.core.maven.TychoMavenLifecycleParticipant.afterProj
    ectsRead(TychoMavenLifecycleParticipant.java:77)
            at org.apache.maven.DefaultMaven.doExecute(DefaultMaven.java:274)
            at org.apache.maven.DefaultMaven.execute(DefaultMaven.java:156)
            at org.apache.maven.cli.MavenCli.execute(MavenCli.java:537)
            at org.apache.maven.cli.MavenCli.doMain(MavenCli.java:196)
            at org.apache.maven.cli.MavenCli.main(MavenCli.java:141)
            at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
            at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.
    java:57)
            at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAcces
    sorImpl.java:43)
            at java.lang.reflect.Method.invoke(Method.java:601)
            at org.codehaus.plexus.classworlds.launcher.Launcher.launchEnhanced(Laun
    cher.java:290)
            at org.codehaus.plexus.classworlds.launcher.Launcher.launch(Launcher.jav
    a:230)
            at org.codehaus.plexus.classworlds.launcher.Launcher.mainWithExitCode(La
    uncher.java:409)
            at org.codehaus.plexus.classworlds.launcher.Launcher.main(Launcher.java:
    352)
    Caused by: java.lang.IllegalStateException: Service is not registered class='int
    erface org.eclipse.tycho.core.facade.ProxyServiceFacade'
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.get
    Service(DefaultEquinoxEmbedder.java:291)
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.get
    Service(DefaultEquinoxEmbedder.java:270)
            at org.eclipse.tycho.osgi.configuration.OSGiProxyConfigurator.afterFrame
    workStarted(OSGiProxyConfigurator.java:30)
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.doS
    tart(DefaultEquinoxEmbedder.java:180)
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.sta
    rt(DefaultEquinoxEmbedder.java:67)
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.che
    ckStarted(DefaultEquinoxEmbedder.java:299)
            ... 34 more
    [ERROR] Internal error: java.lang.RuntimeException: Could not instantiate requir
    ed component: com.google.inject.ProvisionException: Guice provision errors:
    [ERROR]
    [ERROR] 1) Error notifying ProvisionListener org.sonatype.guice.plexus.lifecycle
    s.PlexusLifecycleManager of org.eclipse.tycho.core.TargetPlatformResolver annota
    ted with @com.google.inject.name.Named(value=p2).
    [ERROR] Reason: java.lang.RuntimeException: java.lang.IllegalStateException: Ser
    vice is not registered class='interface org.eclipse.tycho.core.facade.ProxyServi
    ceFacade'
    [ERROR] while locating org.eclipse.tycho.core.TargetPlatformResolver annotated w
    ith @com.google.inject.name.Named(value=p2)
    [ERROR]
    [ERROR] 1 error
    [ERROR] role: org.eclipse.tycho.core.TargetPlatformResolver
    [ERROR] roleHint: p2
    [ERROR] -> [Help 1]
    org.apache.maven.InternalErrorException: Internal error: java.lang.RuntimeExcept
    ion: Could not instantiate required component
            at org.apache.maven.DefaultMaven.execute(DefaultMaven.java:168)
            at org.apache.maven.cli.MavenCli.execute(MavenCli.java:537)
            at org.apache.maven.cli.MavenCli.doMain(MavenCli.java:196)
            at org.apache.maven.cli.MavenCli.main(MavenCli.java:141)
            at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
            at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.
    java:57)
            at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAcces
    sorImpl.java:43)
            at java.lang.reflect.Method.invoke(Method.java:601)
            at org.codehaus.plexus.classworlds.launcher.Launcher.launchEnhanced(Laun
    cher.java:290)
            at org.codehaus.plexus.classworlds.launcher.Launcher.launch(Launcher.jav
    a:230)
            at org.codehaus.plexus.classworlds.launcher.Launcher.mainWithExitCode(La
    uncher.java:409)
            at org.codehaus.plexus.classworlds.launcher.Launcher.main(Launcher.java:
    352)
    Caused by: java.lang.RuntimeException: Could not instantiate required component
            at org.eclipse.tycho.core.resolver.DefaultTargetPlatformResolverFactory.
    lookupPlatformResolver(DefaultTargetPlatformResolverFactory.java:76)
            at org.eclipse.tycho.core.resolver.DefaultTychoDependencyResolver.setupP
    roject(DefaultTychoDependencyResolver.java:86)
            at org.eclipse.tycho.core.maven.TychoMavenLifecycleParticipant.afterProj
    ectsRead(TychoMavenLifecycleParticipant.java:77)
            at org.apache.maven.DefaultMaven.doExecute(DefaultMaven.java:274)
            at org.apache.maven.DefaultMaven.execute(DefaultMaven.java:156)
            ... 11 more
    Caused by: org.codehaus.plexus.component.repository.exception.ComponentLookupExc
    eption: com.google.inject.ProvisionException: Guice provision errors:

    1) Error notifying ProvisionListener org.sonatype.guice.plexus.lifecycles.Plexus
    LifecycleManager of org.eclipse.tycho.core.TargetPlatformResolver annotated with
     @com.google.inject.name.Named(value=p2).
     Reason: java.lang.RuntimeException: java.lang.IllegalStateException: Service is
     not registered class='interface org.eclipse.tycho.core.facade.ProxyServiceFacad
    e'
      while locating org.eclipse.tycho.core.TargetPlatformResolver annotated with @c
    om.google.inject.name.Named(value=p2)

    1 error
          role: org.eclipse.tycho.core.TargetPlatformResolver
      roleHint: p2
            at org.codehaus.plexus.DefaultPlexusContainer.lookup(DefaultPlexusContai
    ner.java:257)
            at org.codehaus.plexus.DefaultPlexusContainer.lookup(DefaultPlexusContai
    ner.java:245)
            at org.eclipse.tycho.core.resolver.DefaultTargetPlatformResolverFactory.
    lookupPlatformResolver(DefaultTargetPlatformResolverFactory.java:74)
            ... 15 more
    Caused by: com.google.inject.ProvisionException: Guice provision errors:

    1) Error notifying ProvisionListener org.sonatype.guice.plexus.lifecycles.Plexus
    LifecycleManager of org.eclipse.tycho.core.TargetPlatformResolver annotated with
     @com.google.inject.name.Named(value=p2).
     Reason: java.lang.RuntimeException: java.lang.IllegalStateException: Service is
     not registered class='interface org.eclipse.tycho.core.facade.ProxyServiceFacad
    e'
      while locating org.eclipse.tycho.core.TargetPlatformResolver annotated with @c
    om.google.inject.name.Named(value=p2)

    1 error
            at com.google.inject.internal.InjectorImpl$3.get(InjectorImpl.java:974)
            at com.google.inject.Scopes$1$1.get(Scopes.java:59)
            at org.sonatype.guice.bean.locators.LazyBeanEntry.getValue(LazyBeanEntry
    .java:83)
            at org.sonatype.guice.plexus.locators.LazyPlexusBean.getValue(LazyPlexus
    Bean.java:49)
            at org.codehaus.plexus.DefaultPlexusContainer.lookup(DefaultPlexusContai
    ner.java:253)
            ... 17 more
    Caused by: java.lang.RuntimeException: java.lang.IllegalStateException: Service
    is not registered class='interface org.eclipse.tycho.core.facade.ProxyServiceFac
    ade'
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.che
    ckStarted(DefaultEquinoxEmbedder.java:301)
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.get
    Service(DefaultEquinoxEmbedder.java:275)
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.get
    Service(DefaultEquinoxEmbedder.java:270)
            at org.eclipse.tycho.p2.resolver.P2TargetPlatformResolver.initialize(P2T
    argetPlatformResolver.java:433)
            at org.sonatype.guice.plexus.lifecycles.PlexusLifecycleManager.initializ
    e(PlexusLifecycleManager.java:338)
            at org.sonatype.guice.plexus.lifecycles.PlexusLifecycleManager.manageLif
    ecycle(PlexusLifecycleManager.java:296)
            at org.sonatype.guice.plexus.lifecycles.PlexusLifecycleManager.onProvisi
    on(PlexusLifecycleManager.java:148)
            at com.google.inject.internal.ProvisionListenerStackCallback$Provision.p
    rovision(ProvisionListenerStackCallback.java:108)
            at com.google.inject.internal.ProvisionListenerStackCallback.provision(P
    rovisionListenerStackCallback.java:55)
            at com.google.inject.internal.ProviderInternalFactory.circularGet(Provid
    erInternalFactory.java:68)
            at com.google.inject.internal.InternalFactoryToInitializableAdapter.get(
    InternalFactoryToInitializableAdapter.java:45)
            at com.google.inject.internal.InjectorImpl$3$1.call(InjectorImpl.java:96
    5)
            at com.google.inject.internal.InjectorImpl.callInContext(InjectorImpl.ja
    va:1011)
            at com.google.inject.internal.InjectorImpl$3.get(InjectorImpl.java:961)
            ... 21 more
    Caused by: java.lang.IllegalStateException: Service is not registered class='int
    erface org.eclipse.tycho.core.facade.ProxyServiceFacade'
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.get
    Service(DefaultEquinoxEmbedder.java:291)
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.get
    Service(DefaultEquinoxEmbedder.java:270)
            at org.eclipse.tycho.osgi.configuration.OSGiProxyConfigurator.afterFrame
    workStarted(OSGiProxyConfigurator.java:30)
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.doS
    tart(DefaultEquinoxEmbedder.java:180)
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.sta
    rt(DefaultEquinoxEmbedder.java:67)
            at org.eclipse.sisu.equinox.embedder.internal.DefaultEquinoxEmbedder.che
    ckStarted(DefaultEquinoxEmbedder.java:299)
            ... 34 more
    [ERROR]
    [ERROR] To see the full stack trace of the errors, re-run Maven with the -e swit
    ch.
    [ERROR] Re-run Maven using the -X switch to enable full debug logging.
    [ERROR]
    [ERROR] For more information about the errors and possible solutions, please rea
    d the following articles:
    [ERROR] [Help 1] http://cwiki.apache.org/confluence/display/MAVEN/InternalErrorE
    xception
    Press any key to continue . . .


Solution: ignore this error at that moment since all builds are successful

Import project into Eclipse

Reference: http://czt.sourceforge.net/dev/eclipse/index.html

1. Download Eclipse Classic 4.2.0
2. Install m2e connectors
   
   • install maven-jflex-plugin and xml-maven-plugin from http://czt.sourceforge.net/dev/eclipse/updates/
3. Install m2e release for Eclipse
   
   • from http://download.eclipse.org/technology/m2e/releases
4. Select the m2e repository cache directory. m2e has caches lucene index in two places
   
   • Per-workspace indexes are stored under .metadata/.plugins/org.eclipse.m2e.core/nexus
   • and there is also global cache in ~/.m2/repository/.cache/m2e/${m2e.version}
5. The default cache directory on Windows in the department is the home directory h:\.WindowsProfile\.m2\. However, this folder has very strict limitation of disk volumn. Thus the cache directory has to be changed.
   
   • Open Eclipse preference, click Maven/Installation. Add external Maven d:\randall\Programs\apache-maven-3.0.5, and unselect the Embedded 3.0.4
   • The settings.xml file will be in d:\randall\Programs\apache-maven-3.0.5\conf. Open settings.xml, and change <localRepository> to <localRepository>d:\.m2\repository</localRepository>
   • Save the changes in Eclipse
6. Open a command prompt window and rebuild the czt-code again
   
   • buildall.bat
   • Now all cached files are saved in the specified directory, and can build successfully
   • Thus the previous Build Error with long error log is due to the limited size of cache repository
7. After the build, open Eclipse and import the czt projects into the Eclipse by File > Import > Existing Maven Projects
   
   • Select the czt-code root directory and import all necessary projects
   • After import, workspace will build automatically
   • Set CZT target platform
     • Open target definition file at /net.sourceforge.czt.eclipse.target/net.sourceforge.czt.eclipse.target.target within Eclipse and clock Set as Target Platform
   • If necessary, right click the project and Maven > Update Projects to update Maven projects
   • If necessary, clean all projects and build again

Setup of a notes writing environment (markdown + Voom + markdown2.py) on Windows

This is a note to write down how to set up a working environment for notes writing efficiently on Windows

Environment Requirement

• VIM editor
• markdown syntax
• Voom outline
• markdown2.py to convert from mkd to html for easily publishing on blog

Install markdown syntax

• Refer to http://www.vim.org/scripts/script.php?script_id=2882
• Download markdown-1.2.2.vba.gz
• Uncompress the gz file and get markdown-1.2.2.vba
• Open the vba file by VIM
• Execute VIM command ":so %"

Install Voom

• Refer to http://www.vim.org/scripts/script.php?script_id=2657
• Download VOoM-4.7.zip
• Uncompress zip file and copy all directories to the $VIM$/vimfiles/
• Open VIM and execute the command ":helptags $VIM/vimfiles/doc"
• Voom does require the python27 installed

Install python27 on Windows

• Install python27 to C:\python27
• Add this directory to the PATH environment variable

Install distribute package to have the packages installation capability (such as pip, easy_install )

• Download distribute package from https://pypi.python.org/pypi/distribute#installation-instructions
• Unpack it, open a command line and execute
  

  python distribute_setup.py

• easy_install.exe is installed in the c:/python27/Scripts
• add c:/python27/scripts directory to PATH environment variable

Install markdown2

markdown2.py is used to convert the mkd file to html file - Open a command prompt window, and type

easy_install markdown2 - Then markdown2.py is installed in the c:/python27/scripts

Test it

• Create a mkd file and write a sample markdown note by VIM
• You should see the syntax works for this file. If not, add "syntax on" vimrc file
• Type command ":Voom markdown" within VIM, and another outline window is opened
• Quit Vim and open a command prompt window, and type
  

  markdown2.py hello.mkd

• Error
  

  close failed in file object destructor: sys.excepthook is missing lost sys.stderr

• Solution: use "python c:\python27\Scripts\markdown2.py hello.mkd > hello.html" instead of "markdown2.py hello.mkd > hello.html"

Concurrency, Parallel, Synchronization and Reactive. How to distinguish them?

Parallel and Concurrent

Parallel

Parallel computing is a form of computation in which many calculations are carried out simultaneously,[1] operating on the principle that large problems can often be divided into smaller ones, which are then solved concurrently ("in parallel"). (from Wikipedia)

Key points of Parallel:

• Usually for time saving and speeding up the calculation
• Decompose the big problem into smaller ones
• The smaller ones run in different processors at the same time
• Reference: https://computing.llnl.gov/tutorials/parallel_comp/#Whatis

Three-level Parallelisms:

• Bit-level (4-bit, 8-bit, 16-bit, 32-bit and 64-bit microprocessors)
• Instruction-level (pipelining (CISC, RISC), superscalar)
• Task-level (multi-processors, tasks running on different processors simultaneously)

Task Parallelism and Data Parallelism:

• Task Parallelism (processes, or threads of execution)

"entirely different calculations can be performed on either the same or different sets of data"

• Data Parallelism

"the same calculation is performed on the same or different sets of data"

Concurrent

Concurrency is a property of systems in which several computations are executing simultaneously, and potentially interacting with each other. (from Wikipedia)

a program is typically factored into multiple threads of control with distinct responsibilities and purposes, which may run simultaneously or take turns. This is often about dealing with concurrency and nondeterminism in the world, or about reducing latency.

Key points of concurrent programming:

• It may run simultaneously on different processors or multithreads on single processor
• the number of possible execution paths in the system can be extremely large and the resulting outcome can be nondeterministic
• Concurrent access of shared resources with nondeterminism may lead to issues such as deadlock and starvation
• What differentiates concurrent system from sequential system most is the fact that their subprocesses communicate with each other

The difference between parallel and concurrency programming

Parallel and concurrent are synonyms in most cases, but in programming, it's not the case. They are totally different concepts.

Example (Parallel and Concurrent programming in Haskell)

A parallel program

• utilize the more powerful and computational hardware (e.g. multiple processors or cores) to make it quickly and achieve more efficiency
• A big task is splitted into several smaller tasks, and each of them is executed in different processor or core at the same time (in parallel). Thus the whole delivery time will be shorter than sequentially performed task

Concurrent program

• concurrency is a progarm-structuring technique in which there are multiple threads of control.
• From the user level, threads are executed "at the same time" because their effects interleaved. But whether they actually execute at the same time or not is not a design problem, and just an implementation detail.
• concurrency can be implemented on one single process with multithreads or on multiple processors
• concurrent programming also concerns program-structuring to interact with multiple independent external agents (for example, one thread responsible for the user, one for database server, and another for external clients)

Distributed, Reactive and Concurrent System

Distributed System

A distributed system consists of multiple computers that communicate through a computer network, and the computers interact with each other in order to achieve a common goal

For example,

• a lithography has several subsystems, and each subsystem runs on its individual embedded system. They are working with central workstation together to achieve the function of the lithography

Reactive System

A system that responds or reacts to external events

For example,

• a motor control driver: it gets the input from the caller or user, then move the motor forward or backward to specified position, and stop
• interactive system is a kind of typical reactive system, which reacts to its user and operators, and provides the feedback

Concurrent System

several computations are running simultaneously and may interact with each other while they are executing.

Architectural Aspect

• Each computer in distributed system has the individual processor and memory
• A parallel system will have the tasks on different processors with shared memory, such as SMP or AMP system
• A concurrent system may have the multiple threads on a single processor or multiple processors with shared memory

Synchronization

Synchronization refers to one of two distinct but related concepts: synchronization of processes, and synchronization of data. Process synchronization refers to the idea that multiple processes are to join up or handshake at a certain point, in order to reach an agreement or commit to a certain sequence of action. Data synchronization refers to the idea of keeping multiple copies of a dataset in coherence with one another, or to maintain data integrity. (from Wikipedia)

CSP (Communicating Sequential Processes)

is a formal language for modelling and reasoning the patterns of interaction in concurrent system

• interaction by synchronous message passing

Parallel

• Synchronous Parallel (P || Q)
• Alphabetised Parallel (P [ Ap || Aq ] Q)
• Generalised Parallel (P [ | a | ] Q, such as P [| {| in, out |} |] Q)
• Interleaving |||

Use VIM to make notes [markdown]

Sometimes you will face a situation that you want to write down some notes, but you can not have a suitable tool on handle. For example, you only have VIM to edit and don't have the "Notes" like Evernote, OneNote etc. So how can you make writing down a note easy? Here's one solution: VIM + Voom + markdown syntax highlight

Source file of this post is reference to markdown.mkd, One screen show:

 

Markdown

Markdown is intended to be as easy-to-read and easy-to-write as is feasible. Markdown’s syntax is intended for one purpose: to be used as a format for writing for the web.

Reference: <http://daringfireball.net/projects/markdown/syntax>

Syntax

Header

Two types of header: Setext and atx

• Setext
  = for 1st level
  
  • for 2nd level
• atx
  # for H1
  ## for H2
  ### for H3
  #### for H4
  ##### for H5
  ###### for H6
  

Block Quotes

• Use the > for each line or only > for each paragraph

Quote Block or

• can be nested

Quote

Block

Bullets

• *, - and + all do the same

Numbering

1. 1 Use the number
2. 2
3. 3

Codeblocks

Indent with 4 spaces or one tab. C Example: for(i = 0; i \< 5; i++) { printf("%d\n", i); }

Horizontal Rules

• three or more (*, -, or _)
  

  ---

  ---

  ---

Links

• Link
  
  • Markdown
  • Markdown
• Reference Style Markdown, Markdown
  
• Automatic link > http://daringfireball.net/projects/markdown/syntax
  

Emphasis

Text wrapped in * and _

• Markdown is very helpful to make notes
• Markdown is very helpful to make notes

Code

Wrap the code with backtick quotes (`) * printf() function will print on the stardard output 0

Special characters

The special characters (\, `, *, _, -, {}, ], (), #, +, ., !) can be inputted by a prefix backslash \

Markdown syntax highlight

Installation

• It's very easy to install it. Just download the latest the markdown-.vba.gz, then
  $ vim makedown-.vba.gz +":so %"
  Reference: http://www.vim.org/scripts/script.php?script_id=2882
  
• Make sure the syntax highlight is on and can be set in .vimrc syntax on filetype on
  

Usage

Just create a new file with extension 'mkd', for example $ vim hello.mkd

Voom - Two-pane outliner

Installation

• Prerequisite: Voom requires the python should be installed
• Download VOoM-.zip
• Unzip it to the ~/.vim/
• Update help tags : helptags $HOME/.vim/doc
  Reference: http://www.vim.org/scripts/script.php?script_id=2657
  

Usage

• Load the markdown format file, such as hello.mkd
• Open Voom markdown markup formats within VIM : Voom markdown

Markups supported

Voom can support a variety of markups - fmr, fmr1, fmr2 -- start fold markers with levels (variations of the default mode);
- wiki -- MediaWiki, headlines are surrounded by '=';
- vimwiki -- vimwiki plugin (vimscript #2226);
- viki -- Viki/Deplate plugin (vimscript #861);
- org -- Emacs Org-mode;
- rest -- reStructuredText section titles;
- markdown -- Markdown headers, both Setext-style and Atx-style;
- hashes -- #, ##, ###, etc. (Atx-style headers, a subset of Markdown format);
- txt2tags -- txt2tags titles and numbered titles;
- asciidoc -- AsciiDoc document and section titles, both styles;
- latex -- LaTeX sectioning and some other commands;
- taskpaper -- TaskPaper (vimscript #2027);
- thevimoutliner -- The Vim Outliner plugin (vimscript #517);
- vimoutliner -- VimOutliner plugin (vimscript #3515);
- cwiki -- vimscript #2176;
- html -- HTML heading tags, single line only;
- python -- Python code browser, blocks between 'class' and 'def' are also nodes.

Convert to html

Installation of python-markdown

• MAC OS: $ sudo easy_install Markdown

Command line

$ markdown_py -f hello.html hello.mkd

Notes: two spaces in the end of line means EOL

Function and its Properties

A function is a relation between input X and output Y with the property that there is at most one element in Y corresponding to each element in X. For example, relation {(1, 2), (1, 3)} is not a function since 1 has two corresponding elements 2 and 3.

If $f: X \to Y$, X is called the domain of function $f$, and Y codomain or range

If $A \subseteq X$, then $f(A)$ is called the image of $A$ under $f$. Refer to the below diagram, the yellow area is image.

If $B \subseteq Y$, then $f^{-1}(B)$ is called the preimage of $B$ under $f$.

From Wikipedia

Identity function
$$id: X \to X \land \forall x: X \bullet id(x)=x$$

Injective function, or one-to-one function
$$\forall a,b:X \bullet f(a)=f(b) \implies a=b$$
For example,

• identity function
• inclusion function
• $f(x)=2x+1$
• $f(x)=e^x$

Inclusion function
$$\forall a:X, b:Y \bullet X \subset Y \implies f(a)=a$$

Surjective function (Onto)
$$\forall y:Y \bullet \exists x:X \bullet f(x)=y$$

From Wikipedia

For example,

• identity function
• $f(x)=2x+1$
• $f: \mathbb{R} \to \mathbb{R}, f(x)=e^x$ is not surjective since there is no x such that f(x) is negative
• $f: \mathbb{R} \to \mathbb{R}, f(x)=x^2$ is not surjective since there is no x such that f(x) is negative
• $f: \mathbb{R} \to \mathbb{R}^{nn}, f(x)=x^2$ is surjective since for each y there is a x that $x^2=y$

Partial Function
A function f from X to Y is partial if it doesn't map every element in X to Y. Formally,
$$\exists x:X \bullet f(x) \text{ is undefined}$$
For example,

• $f: \mathbb{N} \to \mathbb{N}$, and $f(x)=\sqrt{x}$

Total Function
Every element in X is defined.
$$\forall x:X \bullet \exists y:Y \bullet f(x)=y$$
For example,

• $f: \mathbb{N} \to \mathbb{N}$, f(x)=x

Monotonic
$$\forall x_1,x_2:X \bullet x_1 < x_2 \implies f(x_1) < f(x_2)$$

Idempotent
$$\overbrace{f(f(...f}^n(x))=f(x)$$

Associative
$$f(f(x,y), z) = f(x, f(y, z))$$

Distributive
$$f(g(x,y), z) = g(f(x, z), f(y, z))$$
f is distributive in g.
For example,

• $f(x, y) = x \times y, g(x,y)=x+y$, $x \times (y+z)=(x \times y + x \times z)$

Binary Relations and its Properties

Symmetric
$$\forall a, b \bullet a R b \implies b R a$$
where $R$ is a relation. For example,

• = relation on $\mathbb{R}$
• is equal to
• is married to 
• {(1,2), (2,1)}

Antisymmetric
$$\forall a,b:X \bullet a R b \land b R a \implies a = b$$
For example,

• $\leq$
• $\geq$
• $\subseteq$
• {(1, 2), (2, 3), (1, 1)}

Asymmetric
$$\forall a,b:X \bullet a R b \implies \lnot(bRa)$$
For example,

• {(1,2), (3,4)}

Reflexive
$$\forall x:X \bullet xRx$$
For example,

• =
• $\leq$

Irreflexive (strict)
$$\forall x:X \bullet \lnot(xRx)$$
For example,

• $>$, $<$

Coreflexive (a subset of Identity Relation)
$$\forall x,y:X \bullet x R y \implies x= y)$$
For example,

•  equal to and odd, such as {(1,1), (3,3)}

Identity
$$\{(x,x) | x \in X\}$$

Transitive
$$\forall x,y,z:X \bullet x R y \land y R z \implies x R z$$
For example,

• $<$, =, $\leq$

Number Sets in Latex

Include the package amsfonts or amssymb
$\usepackage{amsfont}$ or $\usepackage{amssymb}$

•     Prime Numbers $\mathbb{P}$ ($\mathbb{P}$): No positive divisors other than 1 and itself: 1, 3, 5, 7, 11, ...
•     Natural Numbers $\mathbb{N}$ ($\mathbb{N}$): 0, 1, 2, 3
•     Integers $\mathbb{Z}$ ($\mathbb{Z}$): ..., -3, -2, -1, 0, 1, 2, 3
•     Irrational Numbers $\mathbb{I}$ ($\mathbb{I}$): $\pi$, 1.3333...
•     Rational Numbers $\mathbb{Q}$ ($\mathbb{Q}$): any real number can be expressed by ration of two integers, such as 0.5 (1/2), 1.6 (8/5)
•     Real Numbers $\mathbb{R}$ ($\mathbb{R}$):
•     Complex Numbers $\mathbb{C}$ ($\mathbb{C}$)

Latex enabled in Google Blogger

1. Mathjax
http://www.mathjax.org/

2. Getting Started with Mathjax
http://docs.mathjax.org/en/latest/start.html

3. Open your google blogger and click "Design" on the top right of your home page

Design

4. Click "Edit Html" and paste the following scripts after the first <head> tag

<script type="text/javascript"
  src="http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML">
</script>

The default math delimiters are $ $...$ $ and \ [...\ ] for displayed mathematics, and $...$ for in-line mathematics. Note in particular that the $...$ in-line delimiters are not used by default. If you want to use single-dollars for in-line math mode, you must enable that explicitly in your configuration:

<script type="text/x-mathjax-config">
  MathJax.Hub.Config({tex2jax: {inlineMath: [['$','$'], ['\\(','\\)']]}});
</script>

5. Test in new post

Display Math:

• $ $a^2+b^2=c^2$ $

$$a^2+b^2=c^2$$

• \ [ a^2+b^2=c^2 \ ]

$$a^2+b^2=c^2$$

Inline Math:

• \ ( a^2+b^2=c^2 \ )      $a^2+b^2=c^2$