[Git] work with branch (a new empty branch)

• Create a new and empty branch

$ git checkout --orphan "rye/testmodel"

• Delete all files to make it empty

$ git rm -rf .

• Then add and commit files into the branch

• Finally, push it into remote repository

To push the current branch and set the remote as upstream, use



$ git push --set-upstream origin rye/testmodel

​

[Formal Verification] Hacker-Proof Code Confirmed

A very nice article about application of formal verification. A bit more optimistic about the future of formal specification and verification. Find the article here.

[git] work with tags

1. Create

• lightweight tag

  $ git tag v0.1
  

• annotated tag

$ git tag -a v0.1 -m "my first version"

• tag to a specific commit

  $ git tag -a v0.1 4ba28bf
  

2. Query

• list all tags

  $ git tag
  ether_sysml.v0.4
  ether_sysml_broadcast_unicast_ether.v0.1
  fcu_sysml.v1.0
  fcu_sysml.v1.1
  uav_swarm_sysml.v1.0
  uav_swarm_sysml.v1.0.3
  

• list all tags with annotations

$ git tag -n99
or
$ git tag -n -l

• search with patterns

$ git tag -l "ether*"

ether_sysml.v0.4 ether_sysml_broadcast_unicast_ether.v0.1

• show details of a tag

$ git show ether_sysml.v0.4
tag ether_sysml.v0.4
Tagger: Kangfeng Ye <kangfeng.ye@york.ac.uk>
Date:   Tue Apr 11 20:29:32 2017 +0100

the first version to have Ether with two Ends and create a test project successfully

commit 4ba28bf7e23e091e4d3768814e23204075f66b4c
...

• sort by creation date

$ git for-each-ref --format '%(refname) %09 %(taggerdate) %(subject) %(taggeremail)' refs/tags  --sort=taggerdate
refs/tags/fcu_sysml.v1.0         Wed Mar 15 14:31:32 2017 +0000 V1.0 of FCU test model <kangfeng.ye@york.ac.uk>
refs/tags/fcu_sysml.v1.1          Thu Mar 16 12:55:34 2017 +0000 Update SysML by changing float to double  <kangfeng.ye@york.ac.uk>
refs/tags/uav_swarm_sysml.v1.0   Thu Mar 16 16:07:36 2017 +0000 SysML test model for UAV Swarm <kangfeng.ye@york.ac.uk>
refs/tags/uav_swarm_sysml.v1.0.3          Mon Mar 20 18:11:20 2017 +0000 Correct constant from 2.2 to 1.2  <kangfeng.ye@york.ac.uk>
refs/tags/ether_sysml_broadcast_unicast_ether.v0.1        Tue Apr 4 18:52:35 2017 +0100 This is a tag for the temporary version  to us <kangfeng.ye@york.ac.uk>
refs/tags/ether_sysml.v0.4        Tue Apr 11 20:29:32 2017 +0100 the first version to   <kangfeng.ye@york.ac.uk>

3. Push tags to remote repositories

• a specific tag

$ git push origin v0.1

• all tags

$ git push origin --tags

4. Checkout tags

• checkout a tag into a new local branch

git checkout -b bv0.1 v0.1

Reference:

• https://git-scm.com/book/en/v2/Git-Basics-Tagging
• https://coderwall.com/p/s4ti7q/show-git-tags-with-date-message-and-author

​

[Git] difference between two branches

 Show changes and log between two branches

• $ git diff master..branch
• $ git log master..branch
• $ git shortlog master..branch

Show which files are changed between two branches

• $ git diff --name-status master..branch

Show changes to a specific file between two branches

• $ git diff branch master -- path/to/thefile
• or $ git diff master..branch -- path/to/thefile

References:

• this link (http://linux.yyz.us/git-howto.html#diff_branch)
• this question (http://stackoverflow.com/questions/822811/showing-which-files-have-changed-between-two-revisions)

[Git] how to merge a file from one branch into current branch

Scenario:

• A branch (newbranch) is created and some update on this branch
• Later you want to merge the changes made to a specific file (thefile) on  newbranch to another branch (oldbranch)

Steps:

1. If current working branch is oldbranch, go to Step 4. Otherwise, go to Step 2
2. Clone master branch
3. Fetch all branches and create local branches to track all remote branches (following this post) 
4. Switch to oldbranch, $ git checkout oldbranch
5. Merge by $git checkout --patch newbranch relative_path/to/thefile
• Apply this hunk to index and worktree [y,n,q,a,d,/,j,J,g,e,?]?
• The meaning of each is given with the help of $ git add --help

patch
           This lets you choose one path out of a status like selection. After choosing the path, it presents the diff between the index and the working tree file and asks you if you want to stage the change of each hunk. You can select one of the following options and type return:

               y - stage this hunk
               n - do not stage this hunk
               q - quit; do not stage this hunk or any of the remaining ones
               a - stage this hunk and all later hunks in the file
               d - do not stage this hunk or any of the later hunks in the file
               g - select a hunk to go to
               / - search for a hunk matching the given regex
               j - leave this hunk undecided, see next undecided hunk
               J - leave this hunk undecided, see next hunk
               k - leave this hunk undecided, see previous undecided hunk
               K - leave this hunk undecided, see previous hunk
               s - split the current hunk into smaller hunks
               e - manually edit the current hunk
               ? - print help

[Git] fetch all remote branches and make them tracked by local branches

$ git branch -r | grep -v '\->' | while read remote; do git branch --track "${remote#origin/}" "$remote"; done 

$ git fetch --all
$ git pull --all

Reference from this How to fetch all git branches

[Haskell-Cabal] pass specific options to build tools

Cabal provides options on command line to pass options to specific tools. For example, if we want to pass debug option to happy.

$ cabal build --happy-option=-d

 References:

$ cabal build --help

    --with-PROG=PATH    give the path to PROG
    --PROG-option=OPT   give an extra option to PROG (no need to quote options
                        containing spaces)
    --PROG-options=OPTS give extra options to PROG

The flags --with-PROG and --PROG-option(s) can be used with the following programs:
  alex ar c2hs cpphs gcc ghc ghc-pkg ghcjs ghcjs-pkg greencard haddock happy
  haskell-suite haskell-suite-pkg hmake hpc hsc2hs hscolour jhc ld lhc lhc-pkg
  pkg-config strip tar uhc

[Haskell] add search directories option to ghci

Debug with this

$ ghci src/Test/ParseCircus.hs 

will lead to a problem such as

src/Test/ParseCircus.hs:14:8:
    Could not find module ‘Language.ISOZ.Parser.SynTransformerTwo’
    Use -v to see a list of the files searched for.

Locations searched:
  Language/ISOZ/Parser/SynTransformerTwo.hs
  Language/ISOZ/Parser/SynTransformerTwo.lhs
  Language/ISOZ/Parser/SynTransformerTwo.hsig
  Language/ISOZ/Parser/SynTransformerTwo.lhsig

 To fix it, add more folders to search directories by -i option

$ghci src/Test/ParseCircus.hs -isrc:dist/build

See reference

Transitive Closure and Reflexive-Transitive Closure \(R^+, R^*\)

Closure (Mathematics)

Closure is a property said to be satisfied by a set under a given operation if and only if performing the operation on members of the set always produces a member of the same set. (Wikipedia)

• binary relation: 2-ary relation (\(R \subseteq S \times S\))
• P closure operator: cl(R) is the strongest or the smallest relation (\(cl(R) \subseteq S \times S\)) that contains R (\(R \subseteq cl(R)\)) and the property P holds (P(Q)=true).
• a binary relation R is transitive: \(\forall x,y,z: S \bullet (((x,y) \in R \land (y, z) \in R) \implies (x,z) \in R)\)
• for example, \(>, =, \geq, \leq\) are transitive, but "is parent of" is not.
• a binary relation R is reflexive: \(\forall x: S \bullet ((x,x) \in R)\)
• for example, \(=,\geq,\leq\) are reflexive, but > is not reflexive

For example,

• reflexive closure: \(cl_{ref}(R)\) is the smallest relation that contains R and is reflexive.
• transitive closure: \(cl_{trn}(R)\), or \(R^+\) is the smallest relation that contains R and is transitive.
• reflexive–transitive closure: \(R^*\) is the smallest relation that contains R and is both transitive and reflexive.

Definitions

• \(R^r=R \cup id\ S\) - reflexive closure
• \(R^s=R \cup R^\sim\) - symmetric closure 
• \(R^*=R^+ \cup id\ S\)

Alternative Definitions in terms of iterations (Z notation)

• iteration of relation: \(R^k=R;R;...;R = R;R^{k-1}=R^{k-1};R\)
• \(R^0=id\ S\)
• \(R^+=\bigcup\{k:\mathbb{N}_1 \bullet R^k\}\) 
• \(R^+=\bigcup\{k:\mathbb{N} \bullet R^k\}\) 

Applications

• transitive closure of a directed graph likes cities connection by railways or airplanes: means all possible routes from one city to another city, then can be used to calculate the shortest path from one place to another place
• \(R = \{(A,B),(B,C),(B,D),(C,A)\}\) - direct routes between two cities
• \(R^2=R;R=\{(A,C), (A,D),(B,A),(C,B)\}\) - one stop routes between two cities
• \(R^3=R^2;R=\{(A,C), (A,D),(B,A),(C,B)\};\{(A,B),(B,C),(B,D),(C,A)\}=\{(A,A),(B,B),(C,C),(C,D)\}\) - two stop routes between two cities
• \(R^4=R^3;R=\{(A,A),(B,B),(C,C),(C,D)\};\{(A,B),(B,C),(B,D),(C,A)\}=\{(A,B),(B,C),(B,D),(C,A)\}\) - equal to R
• finally, \(R^+=R \cup R^2 \cup R^3=\{(A,B),(B,C),(B,D),(C,A),(A,C), (A,D),(B,A),(C,B),(A,A),(B,B),(C,C),(C,D)\}\)

Example

[Logic] Arguments, Validity, Soundness and Completeness

Arguments:

In logic and philosophy, an argument is a series of statements typically used to persuade someone of something or to present reasons for accepting a conclusion [Wikipedia]

An argument consists of one or more premises and only one conclusion.

Another reference is here.

 Deductive arguments

The conclusion is a logic consequence of the premises. It is based on the premises and then the conclusion follows necessarily.

 Inductive arguments

An inductive argument is an argument that is intended by the arguer merely to establish or increase the probability of its conclusion. [Encyclopedia]

 Validity

 A valid deductive argument guarantees the truth of the conclusion provided the premises are true, regardless of the reality of the premises, by following logic form. Being a valid deductive argument, if all premises are true, the conclusion is impossibly false (must be true).

A --> B
A
--------
B

This is a valid argument no matter whether A and (A-->B) are possibly true or not in real.

Soundness

A sound argument is a valid argument and the premises are true in real.

Validity vs. Soundness

In the example above,

• if A and B stand for "All trains travel faster than cars" and "No one will travel by car", then the argument is valid but not sound because two premises are not true in real. 
•  The argument such as  "All even numbers can be divided by 2; 4 is a even number; therefore 4 can be divided by 2", is valid and sound.

Completeness

A system is said to be complete if something is really true, the system is capable of proving it.

Soundness vs. Completeness

A good way to understand these definitions is that soundness prevents false negatives and completeness prevents false positives. [from note]

False negatives mean "tested to be true actually it is false". Soundness prevents "something is said to be true but actually is not true". It guarantees that "if something is said to be true, it really is true."

False positives mean "tested to be false actually it is true". Completeness prevents "something is said to be false but actually is not false". It guarantees that "all true things are provable."

A sound logic proves only true things. A complete logic proves all true things. [from note]

Shift/Reduce demonstration - 2 [Happy]

Happy is a LALR(1) parser.

The production: (to get an expression)

Expr16 :: Expr16 'cross' Expr17
             | Expr17

 The syntax to demonstrate:

ZED X == A x B x C END

Shift/Reduce demonstration - 1 [Happy]

Happy is a LALR(1) parser.

The production: (to get an expression)

Expr16 :: Expr17 'cross' Expr16
             | Expr17

 The syntax to demonstrate:

ZED X == A x B x C END

1st part

2nd part

Summary

Shift/Reduce demonstration - 0 [Happy]

Happy is a LALR(1) parser.

Left Associativity

The production (as shown).
Two expressions ( 1 + 1 + 1, and 1 + 1 * 1)  are demonstrated.

 

Finally, Exp3 will be reduced to Expression.

Right Associativity

The production (as shown).
One expression ( 1 + 1 + 1)  is demonstrated.

Finally, Exp3 will be reduced to Expression.

 

LL, LR, LALR, GLR ...

• Top-down parser

Beginning with the start symbol, try to guess the productions to apply to end up at the user's program. An example from this slide is shown below

 


First it starts from E and guesses "E --> T + E" to apply, then "T --> int", and "E --> T", " T -> (E)", "E --> T + E", "T --> int", "E --> T", finally "T --> int"


•  LL(1) 
• first 'L' - read the input from left to right.
• second 'L' - descend into parse tree children from left to right (Leftmost derivation).
• 1 - a single lookahead token 
• Predict/match parser

• LL(2)
• 2 - two lookahead tokens

• Bottom-Up parser

Beginning with the user's program, try to apply productions in reverse to convert the program back into the start symbol. Another example from this slide is illustrated.

 

 Start from "int + (int + int + int)", apply the reverse of the production "T -> int": "int -> T" and get 

• int -> T :           T + (int + int + int)
• T -> E:              E + (int + int + int)
• int -> T:            E + (T + int + int)
• T -> E:              E + (E + int + int)  
• int -> T:            E + (E + T + int)
• E + T -> E:       E + (E + int)
• int -> T:            E + (E + T)
• E + T -> E:       E + (E)
• (E) -> T:           E + T
• E + T -> E:       E

• SLR
• Simple LR(1)
• LR(0), LR(1), LR(k)...
• first 'L' - read the input from left to right.
• second 'R' - reversed Rightmost derivation.
• 1 - a single lookahead token 
• LR(1) is very powerful
•  LALR
• Look-Ahead LR parser is a variant of LR
• LALR(1): Look-Ahead (1) LR(0)

•  GLR
• generalized LR: an extension of LR
• handle nondeterministic and ambiguous grammars

• Shift/reduce parser 
• A parsing method for LR parser
• Split input stream into two substrings: only process left substring and right substring is unseen.
• Shift: move the separate bar in the input stream by one token (left to right)
• Reduce: apply productions to left substring to get a new parser tree
• Shift/Reduce conflict: an error where a shift/reduce parser cannot tell whether to shift a token or perform a reduction.
• Often happens when two productions overlap.
• Reduce/Reduce conflict: an error where a shift/reduce parser cannot tell which of many reductions to perform.
• Often the result of ambiguous grammars.
• Reference: this slide and this video