-- PREFACE

--This is my proposed language for the new model checker called SyMP
--that I'm going to write.  

--The main purpose for the language at the moment is to provide a
--"universal" language translatable to SMV and BMC/DIMACS formats, and
--capturing most of the features used in state-of-the-art model
--checkers, so that specs in other languages can be cleanly translated
--to it.  Thus, it will serve as a bridge between many languages.

--It is also supposed to have clean syntax and semantics, and be "fool
--proof" in many ways, so that I will not be bugged by dozens of people
--asking me stupid SMV-language related questions.

--Putting it in other words, you should not be able to write a program
--that has a non-intuitive or non-intended semantics.  It you write
--"Manchester", it should not mean "Liverpool".

-- COMMENTS

-- I like SMV comments.  Leave them.

(* I also like ML comments.  
    (* And make them recursive as well. 
       (* If I figure out how to do this *) *) *) -- but don't use them so far.

-- INCLUDING FILES

-- Now to the real stuff.  Keywords are not case-sensitive (like in PVS),
-- but identifiers are.  So, TYPE == type, but Boo != boo.

include("file.symp") -- simple but useful feature

-- TYPES

type MyType = -5..5; -- `;' is optional when unambiguous

-- Only non-recursive datatypes are allowed so far.
-- This is a model checker, everything has to be finite.
-- You can reference other datatypes though, as long as there
-- is no circularity.

--Types can be infinite though (like `int').  But they cannot be used to
--declare state variables directly, unless the type is symmetric.  More
--on that below.

-- Every type declaration is a different type.  You can't cast values
-- between types, except for subranges (will consider it later).
datatype state = one | two | three

datatype device = cache of state | bridge 

-- Anonymous types are ok.  Multiple declarations of the same
-- anon type are allowed, but they have to be consistent.
-- Parens can be used wherever there may be an ambiguity.
type Arr = array MyType of (device * (idle | busy))

type OtherArr = array (idle | busy) of Arr

-- Unlike in PVS, I don't allow fields of records to depent
-- on each other.  It could be useful for the user, but
-- devilishly hard for the implementor...  Not for now, at least.
type State = { state: state, arr: Arr }

-- In general, every value or type is treated the same if it looks
-- the same.  However, everything has to be well-typed, including
-- constants, and this precludes from having the same constructor in
-- two different datatypes.

-- SYMMETRIC TYPES

--They are types that are supposed to be used in such a way that any
--permutation of values of variables of these types would not change the
--semantical state of the program.  The only permitted operation on the
--values of such types is equality.  You can also have a variable of
--that type as an index of an array, or as an argument to a function
--defined on that type.  The body of the function, however, has to
--preserve the symmetry as well.

--I do not allow breaking the symmetry yet, as in Ken's SMV.  Maybe I'll
--implement this feature in the future if I find it necessary, but I do
--not like the idea, since it's not clean PL-wise.  I hope there is a
--better way to achieve the same thing.

type snat = symmetric nat

datatype Move = symmetric go | walk | step | chug

-- TYPED NAMES

-- Variable declarations.  Note: these are not state variables.
-- These are *names* that can be used as variables with types already
-- pre-assigned to them.  No need to specify a lot of types everywhere.
-- Like in PVS.

var ar: idle | busy
var x,i,j,k: MyType

-- CONSTANTS

-- Constants like in ML.  You can't change their values.
val default_ind: MyType = 0

-- Variable types can be changed locally, if needed.
-- Also, some pattern machting is done as in ML, and
-- here's how to extract a tuple's element:
fun inc(ar: Arr, x): device = let val (d,_) = ar(x) in d end

--Didn't I say that functions can be declared by cases using pattern
--matching?  In this case, if the type of the pattern can be uniquely
--determined, you don't have to specify it.  However, you still need to
--specify the type of the result at least in one of the branches.
fun state2nat(one): nat = 1
  | state2nat(two) = 2
  | state2nat(three) = 3

--Unlike in ML, functions cannot be recursive, and thus, you can always
--define the same function in the "lambda" form:

val inc1: Arr * MyType -> device =
   fn (ar: Arr,x): device => let val (d,_) = ar(x) in d end

--So far you have to specify the type twice in this case, which is
--clearly redundant and may change in future.  But it's always safe
--to do so anyhow.

-- Note, that type declarations are *obigatory*, unlike in ML, either
-- explicitly, or by declaring a variable name (var).
-- In particular, the result type of a function *must* be explicit.

-- OVERLOADING

-- In general, identifiers can be overloaded, as long as there is a way
-- to resolve it.  It may be not as general as in PVS though.
-- Different non-functional constants can be resolved by specifying
-- their types when they are used, or by the context.
-- Functions should have different number or types of arguments, or 
-- different result types.

--The resolution algorithm (proposed, inefficient): list all the
--possible types for the topmost function.  For each type, try to
--propagate it down to the arguments and recurse on the arguments.
--Collect all the sucessful type assignments.  If it is not exactly one
--type, signal an error.

-- MODULES

--Modules are similar to SMV modules in spirit, but with some
--significant improvements.  First, there are two kinds of parameters:
--static and "dynamic".  Static ([...]-parms) are those that can be
--computed at compile time and are here only to code a class of similar
--modules with different parameters in one declaration.

--The way static params are used is the following.  At the module
--instantiation, after the first quick typechecking, a new declaration
--of the module is being created with the concrete values instantiated,
--and then this copy (presumably, automatically type-correct) is used as
--the instance.  For example, translating this into SMV would require
--decraring a new module for each set of static params used in the program.

--Because of that, static params can be of infinite types (int), or can
--be types themselves.  They can also depend on each other (from left to
--right).  I may disallow that, however, if it turns out to be too difficult
--to implement.

--The other set of params ("()"-params) are inputs to the module.  This
--is the way the module communicates with the other modules.  These
--inputs will become equivalent to the expressions at the module's
--instantiation, or will be non-deterministic if the module is used as
--the top module.

-- The dynamic params can use static ones for type declarations.

--Both kinds of the parameters are optional, but the order in which they
--are used together is important: first static, then dynamic.

-- A module with static params cannot be used as the top module in
-- general.  More on that to follow.

MODULE foo[N: int, type T, ar: array 0..N-1 of T](x,y: bool, s: T) =
BEGIN

var s, out: T -- These are just local names, not any objects yet.

StateVar l1,l2,boo: MyType; -- and these are actual state vars

--A state var can be a function.  No problem.  Functions are first class
--objects, and they can be recomputed as we go.  The only restriction is
--that both domain and range have to be either a finite type or a
--symmetric type.  Then the function is the same as an array.
--In particular, accessing array element is denoted as arr(0), not arr[0],
--since it is a function call.

StateVar moves: snat -> Move

-- No type, it was already pre-assigned
StateVar out
-- This will be an output.  It becomes visible outside of the module.
-- Note the difference from PVS, where everything is visible.
-- Here nothing is visible outside unless it is exported.
export out

-- You can also export local constants, so you can use a module as
-- a function library, or a configuration specifier, not only as a
-- supply of new state variables.

fun dec(i): MyType = if i>-5 then i-1 else undefined endif
export dec

--And you can export all the objects in the module at once using the
--`all' keyword:

export all

--Notice another feature: `undefined' value.  Every type has a one more
--implicit value which is assigned whenever there is a run time error.
--You can also assign it explicitly with the `undefined' keyword.  This
--value is defined for *every* type.  If the type of `undefined' is
--ambiguous, then you have to specify it explicitly (undefined: MyType).

--This is the instantiation of a module.  Note, that this is not yet
--included in the state space, it is just a name for a particular
--instance of it.  In fact, this is just another module declaration,
--same good as with the BEGIN-END clause.  So, modules can be
--declared locally, with arbitrary nesting and the same visibility
--rules.  You can export a local module to make it visible outside.

module b1 = bar[N,T](max(l1,l2))

--Applying the rule that everything that looks the same is the same
--object, if you declare another constant, say b2, to be the same
--instance of the module, you get exactly the same module again.
--That is,
--module b2 = bar[N,T](max(l1,l2))
--is the same now as
--module b2 = b1
--No more, no less.

--In particular, if `bar' had an object `x' in it exported, then
--referring to b1.x, b2.x and bar[N,T](max(l1,l2)).x would be
--indistinguishable.

--If you want to have multiple copies of a module that are truely different,
--make a ghost static parameter to that module.  For instance, declare

module bar_i[inst, N: int, T: TYPE](l: MyType) = ...
--and use it as
module b[x: nat] = bar_i[x,N,T](max(l1,l2))
module bb1 = b[1]
module bb2 = b[2]

--Notice, however, that you can't trick the system by "wrapping" the
--original `bar' into another parameterized module, like

module wrapper[i: nat] = bar[N,T](max(l1,l2))
module w1 = wrapper[1]
module w2 = wrapper[2]

--In the last case w1 and w2 are again one and the same object, since
--the body of `wrapper' is the object that does not depend on `i'.

--In fact, this is true even for `bar' declared with the extra parameter
--`inst', if it doesn't have state variables.  State variables are
--exceptional in this case.  If a module is defined with the begin-end
--clause, then state variables are assumed to depend on all of the
--static parameters.  All the other objects in the module depend only on
--those parameters that they *explicitly* depend on.  As an example,
--declare

module moo[i: nat] =
begin
  StateVar meaou: bool;
  module b = bar[N,T](max(l1,l2))
  export meaou, b
end

--Now, the two objects moo[0].meaou and moo[1].meaou are two distinct
--state variables (since they are assumed to depend on `i').  But
--moo[0].b and moo[1].b is again one and the same module, since it does
--not depend on `i'.  In particular, any state variables of moo[0].b
--will be the same state variables as in moo[1].b.  Think of them as
--just having several different names.

--Notice also the visibility rules: you can always see objects outside
--of the module, unless they are shadowed by a local declaration.  In
--the latter case, there is no way to reference the outer object by that
--name.

--The only exception to this rule are again state variables.  They can
--only be seen from outside if exported, by cannot from inside.  That
--is, you cannot read state variables of your parent module directly.
--Exactly for that purpose we have the dynamic parameters: to export
--state variables into local modules.  This restriction has to do with
--the semantics of the transition relation.  It is not clear to me what
--it's going to be if you can read any variable outside of your world if
--you want to prove a general theorem for your module.  You will
--probably see the problem when we get to specifications.

--the `open' construction allows you to declare names for all the
--exported variables of a local module on the current level.

open moo[3]

--After this statement, all the objects of the form `moo[3].x' will be
--renamed to just `x'.  There is nothing special to it, just syntactic
--renaming.

-- TRANSITIONS

--Similar to SMV, a module can have a transition relation associated
--with its state variables.  However, you can only define transitions on
--your own local state variables.  The state variables of other modules
--and dynamic inputs cannot be assigned to.  If you want to communicate
--something _to_ another module, export a designated state variable, or
--declare a local instance of the module with that state variable as a
--dynamic parameter.

--Again, as in SMV, there are three types of assignments: "normal"
--(invariant), init(), and next().  Each variable can only have at most
--one either normal or next() asignment.  In the case of a next()
--assignment, the variable also *has* to have an init() assignment.

--Unlike in SMV, however, if a variable `x' is not assigned anything,
--then it is assumed to have a `next(x) := x' assignment with the
--consequence of having to have an init(x) assignment.

--A variable cannot have a normal assignment in one place and a next
--assignment in another place of a program, even if the assignments
--never collide.  More on that later.

  init(l1) := 0;

-- Nondeterminism is expressed as `|'-separated values.  This "value" is
-- a first-class object, and can be mixed with other operations.
-- ... Unless I find it hard to implement right...
--Notice, that you can use init values of vars defined earlier.
--You can't use l2 here yet though.  This breaks circular dependences.
  init(boo) := (l1 | 1 | 2);

-- Any value of the var's type can be assigned non-deterministically
-- with the `anyValue' keyword.  (Think of a better name for it?)
-- As with `undefined', this literal is overloaded for all the types,
-- and may have to be type-constrained to typecheck.
  next(l1) := anyValue

-- Normal assignments can also have nondeterminism.  Remember that the
-- semicolon at the end is optional.
  l2 := l1 | boo

--No ugly DEFINE statements.  Instead, you can use functions or
--`let'-variables:

  x := inc(y);

  let val IamMacro = inc(x)
  in next(y) := IamMacro
     next(zoo) := y | IamMacro
  end

--As you see, you can group assignments inside the scope of certain
--control structures.  Here is a more interesting example of grouping:

  if x > 0 then
    next(x) := y;
    next(y) := x
  elsif x = 0 then
    next(x) := y;
    next(y) := y;
  else
    next(x) := inc(x)
  endif

--Notice the difference in syntax from ML: `if' ends with `endif'.  The
--open-ended if's, and especially case's always bug me in ML.  This is
--my chance to make it right finally.

--Another important feature is multiple `next' assignments to the same
--variables in different branches.  This is considered ok, as soon as at
--the end only one assignment can possibly execute at a time.  The
--algorithm to determine that is the following.  First, the `if' or
--`case' statements are duplicated for each variable, so that each group
--contains only one variable, and then the assignments are "lifted up"
--to the top level.  After this process there must be only one normal or
--`next' assignment for each variable, like in SMV.

--All of the assignments are executed in parallel.  You cannot have a
--chain of normal assignments like (z := y; y := x; x := z) and expect
--it do "the right thing".  Instead, you'll have to do it with
--`next': (next(x) := y; next(y) := x).  The value of x will not be
--affected at the current cycle by the `next(x) := y', and `y' will receive
--the original value of `x'.

case moo[0].meaou of
    true => next(dah) := l1 | l2
  | false => noop
endcase

--There are two interesting points in the above case statement.  First,
--it ends with `endcases' - no need to parenthesize it all along.
--Second, there is nothing to do when moo[0].meaou=false.  You always
--*have* to provide an operator, and if you decide not to, put a `noop'
--keyword to express that explicitly.  The idea of the language is to be
--explicit and clear in as many aspects as possible.

--The case statement has to cover all the cases.  There is no `else'
--construct, however.  Instead, like in ML, you can match the other
--values with a variable pattern, or `_'.  The typechecker should be
--able to determine if you covered all of the cases or not.  You can use
--any patterns in the cases, like in function declarations.

--The next is a new construct of "guarded commands".  There is no analog
--in SMV.  Each branch of the `choose' statement for which the guard is
--true can be chosen for execution nondeterministically.  Thus, the
--order of the guards is unimportant (unlike in the case or if statements).

choose
    l1 = 1 => next(l2) := l1
  | l2 = 1 => next(l1) := l2
  | true => noop
endchoose

--Although `noop' is executed by default when no guard is true, the last
--guard is not redundant.  In this case it allows stuttering even if
--both of the previous guards are true.  Be careful with this statement,
--it's not always intuitive to use, and it's probably better to avoid it
--if you can.

--I may also postpone the support for `choose' since I'm not sure how to
--check for the "single assignment" condition here yet.  Maybe it's not
--that hard, we'll see.

-- NO DEFINES???

--Often it is desirable to have special macros that stand for complex
--expressions, and be able to export them.  Don't do it in this
--language.  Create a new state variable for that purpose.  The parser
--should be able to detect all variables that depend deterministically
--on other variables and prune them out of the state.  So, in a way,
--they will automatically become "DEFINE" macros.  You just don't have
--to worry about it anymore.

-- MORE EXPRESSIONS

--There will be usual arithmetic (+, -, *, =, !=, <, >, <=, >=, mod,
--div, ...)  and boolean (and/&, or, implies/->, not/!, ...)
--expressions.

--Quantifiers over finite types:

  forall (i: MyType): moo[i].meaou
  exists (i: MyType): moo[i].meaou

--The `if', `case', and `let' expressions can also return values.  There
--are examples above.  In addition, records can be updated by fields
--using `with' statement.  I desperately want this in ML, and I'll
--include it here.

StateVar s,q: State;

  s := q with [ state := two ]

-- I hope I can convince the type checker to figure out the next line
-- automatically:
  init(q) := { state = one, Arr = fn (x) => (bridge,idle) }
  next(q) := s with [ Arr(0) := s.Arr[1] ]

--A record field can be extracted using `.' notation, or by pattern
--matching as in ML:

  state := let val { state = s, ... } = q 
           in s end;

--I will be adding more expressions, of course.  I just can't think of
--all of them right now.

-- PARALLEL COMPOSITION

--Modules can be composed in parallel both synchronously and
--asynchronously.

--Asynchronous composition is done using a single bar `|', and
--synchronous - with double bar `||'.  To better remember which is
--which, think of a `|' as an `alternative' operator, like anywhere else
--in the language.  Thus, you nondeterministically choose one of the
--modules for execution.  The `||' looks "more parallel", thus it's a
--truely synchronous execution in lock-step.  SYmple enough.

module b1b2 = b1 | b2
module b1b2moow2[i: nat] = (b1 | b2) || moo[i] || w2

--Another way to express synchronous and asynchronous composition of
--parameterized modules is by using `sync' and `async' expressions.  As
--with quantifiers, only finite or symmetric types are allowed as the
--bound variable range.

module moo_all = sync(i: MyType): moo[i]
module moo_any = async(i: MyType),(j: snat): moo[i] | b1b2moow2[j]
module xxx[type finite FT](s: FT) = qqq(s) | (sync(i: FT): b1b2moow2[i])

--A keyword `finite' is used to inform the typechecker that the
--parameter type has to be finite (its use is similar to `symmetric'
--keyword).  A `finite type' can be instantiated by any finite type.

--You can also declare any type to be `finite' explicitly.  This may
--simplify the typechecking process.

--As you can see, composition is just another way of a module
--declaration.  And as for most of objects in the language, you can
--refer to `b1b2' both by its new name, or as `b1 | b2'.  They represent
--exactly one and the same object, since they look the same.

--You can only compose modules that are declared locally.  You cannot
--refer to the name of any outer modules.  The reason is the ambiguity
--in static parameters that arises in this case.

--The only exception is the current module.  If you use the current
--module, however, you cannot specify its parameters, both static and
--dynamic.  It is useful to allow that to be able to model check certain
--properties for a module in general, once and for all, and then use
--that theorem in any instance of that module without reproving it.

-- SPECIFICATIONS

--There are no "pure" specs as in SMV.  All the properties are expressed
--as theorems, and each theorem is always self-contained.  For example:

lemma lem_1 = moo[N] implements b1b2

lemma lem_2 = b1b2 |= AG(b1b2.noerror)

theorem myFirstTheorem = foo || moo[N] |= AG(moo[N].noerror)

--Any of the following keywords can declare a theorem, and all of them
--are semantically identical:

--theorem, lemma, proposition, spec, specification, corollary,
--conjecture.

--I may be adding more of them.  Also I will leave the theorem
--expression to be open for other things like fairness constraints,
--assumptions, (limited) quantifiers, etc.  So far let it be the
--`implements' (or `refines', or `simulates' for the reverse)
--expression, and the `<module> |= <CTL formula>' statement.

--Since the current module may appear on the LHS, and it may have static
--parameters, it is not always possible to prove such a theorem in
--general.  (Remember, we're in the MC world!)  However, if all of the
--static parameters are of finite types, then the module can be
--instantiated sufficiently many times, and the theorem will be proved
--for each instance separately.  This process may involve symmetry
--reduction, and the actual number of instances may not be as large.
--So, this feature can be beneficial in the case when a concrete
--instance of the module used later is too big.

-- With static parameters uninterpreted constants, functions, and even
-- types become completely natural - they are simply parameters to the
-- module, and thus, can be anything.  Moreover, instantiating a module
-- will automatically create particular instances of all proven theorems
-- of the module.  This is precisely what uninterpreted functions are
-- made for.

--Another subtlety is what exactly is the state space for the current
--module.  To answer that question, take the spec you are about to
--prove, do the cone of influence reduction, take all the variables that
--are relevant, including the ones in local submodules, assume dynamic
--inputs to be completely nondeterministic (thus, they also become state
--variables), and you get your state.  Then you can do some variable
--reductions, like the one I mentioned for implicit DEFINE's, and you
--can have a refined notion of a state.

--So far I do not allow mixing several such expressions in one theorem.
--This may change in the future.

--Also be careful not to mention any state variables in the CTL formula
--that do not appear in the module on the LHS of `|='.  This is not
--allowed.  And it doesn't make any sense either.

END   -- end the module.

-- TOP LEVEL ENVIRONMENT

--At the top level you can define anything but state variables.  I don't
--think there is any good reason to define state vars here anyway.

--Also, there is no "the top module" notion any longer.  Any module can
--serve the purpose of a "top" module, depending on the theorem you are
--currently trying to prove, and provided it has a "good" set of static
--parameters.

--Since the top level is not a first class module, any theorem at the
--top level has to refer to some module.  It cannot be just a CTL
--formula out of the air.q

--This notion of the top environment may change, however.