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