1
2(******************************************************************************
3* Command line tool
4*
5*  pslcheck [-all] -sere '<SERE>' -path '<PATH>'
6*  pslcheck [-all] -fl   '<FL>'   -path '<PATH>'
7*
8* The optional "-all" argument specifies that all intervals are
9* checked in the case of a SERE and all path tails in the case of a
10* formula.
11*
12* Without the "-all" arguments, the commands:
13*
14*  pslcheck -sere '<SERE>' -path '<PATH>'
15*  pslcheck -fl   '<FL>'   -path '<PATH>'
16*
17* report "true" or "false" (or a parser or processing error).
18*
19* The command:
20*
21*  pslcheck -all -sere '<SERE>' -path '<PATH>'
22*
23* reports "true on intervals [m1:n1][m2:n2] ..."
24* (or a parser or processing error).
25*
26* The command:
27*
28*  pslcheck -all -fl   '<FL>'   -path '<PATH>'
29*
30* reports "true at times t1,t2, ..."
31* (or a parser or processing error).
32*
33* Arguments have to be in the order shown here.
34******************************************************************************)
35
36open HolKernel Parse boolLib bossLib;
37open ParserTools;
38
39val _ = print (process_args(CommandLine.arguments()) ^ "\n")
40
41(*
42pslcheck      -sere '{{a;b}@clk1;c}@clk2' -path '{clk2}{clk1,a}{a}{clk1,b,clk2}{c}{clk1}{c,clk2}{clk1}'
43pslcheck -all -sere '{{a;b}@clk1;c}@clk2' -path '{clk2}{clk1,a}{a}{clk1,b,clk2}{c}{clk1}{c,clk2}{clk1}'
44
45pslcheck      -fl '(a until! b)@clk' -path '{}{clk}{}{clk,a}{a}{clk,a,b}{}{clk,b}{b}{clk}'
46pslcheck -all -fl '(a until! b)@clk' -path '{}{clk}{}{clk,a}{a}{clk,a,b}{}{clk,b}{b}{clk}'
47*)
48