Skip to content
Snippets Groups Projects
Commit bca957fc authored by Jaime Arias's avatar Jaime Arias
Browse files

add maude files

parent a56eab5a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2341 additions and 881 deletions
README.md
+ 7
− 9
View file @ bca957fc
# pta2maude
# nptav2maude
We give a rewriting logic semantics for parametric timed automata (PTAs) and
show that symbolic reachability analysis using
We give a rewriting logic semantics for parametric timed automata with global
variables (PTAVs) and show that symbolic reachability analysis using
[Maude-with-SMT](https://maude-se.github.io/) is sound and complete for the PTA
reachability problem. We refine standard Maude-with-SMT reachability so that
the analysis terminates when the symbolic state space of the PTA is finite.
Besides reachability, the rewrite theory can be also used for parameter
synthesis. This repository includes benchmarks comparing our methods and
reachability problem. We refine standard Maude-with-SMT reachability so that the
analysis terminates when the symbolic state space of the PTA is finite. Besides
reachability, the rewrite theory can be also used for parameter synthesis. This
repository includes benchmarks comparing our methods and
[Imitator](https://imitator.lipn.univ-paris13.fr/).
Details about the translation can be found in [this paper](./paper.pdf).
## Getting started
The project was tested in [Maude 3.2](http://maude.cs.illinois.edu/) and [Maude
......
maude/alt-smt.maude 0 → 100644
+ 332
− 0
View file @ bca957fc
***(
Extending BOOL, RAT and INT with SMT variables of the form bb(x), ii(x)
and rr(x)
BoolExpr (Bool extended with SMT variables) expressions can be checked for satisfiability
using smtCheck that transforms a BoolExpr into a BoolExpression
)
load smt .
load smt-check .
fmod ALT-BOOLEAN-EXPR is
including VAR-ID .
including BOOL .
sort BoolExpr .
subsort Bool < BoolExpr .
sort BoolVar .
subsort BoolVar < BoolExpr .
op bb : SMTVarId -> BoolVar [ctor] .
op not_ : BoolExpr -> BoolExpr [ditto] .
op _and_ : BoolExpr BoolExpr -> BoolExpr [ditto] .
op _xor_ : BoolExpr BoolExpr -> BoolExpr [ditto] .
op _or_ : BoolExpr BoolExpr -> BoolExpr [ditto] .
op _implies_ : BoolExpr BoolExpr -> BoolExpr [ditto] .
op _===_ : BoolExpr BoolExpr -> BoolExpr [comm prec 51] .
op _=/==_ : BoolExpr BoolExpr -> BoolExpr [comm prec 51] .
op _?_:_ : BoolExpr BoolExpr BoolExpr -> BoolExpr [gather (e e e) prec 71] .
vars A B C : BoolExpr .
--- from BOOL-OPS
eq true and A = A .
eq false and A = false .
eq A and A = A .
eq false xor A = A .
eq A xor A = false .
---(
eq A and (B xor C) = A and B xor A and C .
eq not A = A xor true .
eq A or B = A and B xor A xor B .
eq A implies B = not(A xor A and B) .
---)
eq true implies A = A .
eq false implies A = true .
eq A implies true = true .
--- some basic equations
eq A === A = true .
eq (true === false) = (false).Bool .
eq (true =/== false) = (true).Bool .
eq true ? A : B = A .
eq false ? A : B = B .
endfm
fmod ALT-INTEGER-EXPR is
protecting ALT-BOOLEAN-EXPR .
including INT .
sort IntExpr .
subsort Int < IntExpr .
sort IntVar .
subsort IntVar < IntExpr .
op ii : SMTVarId -> IntVar [ctor] .
op -_ : IntExpr -> IntExpr [ditto] .
op _+_ : IntExpr IntExpr -> IntExpr [ditto] .
op _*_ : IntExpr IntExpr -> IntExpr [ditto] .
op _-_ : IntExpr IntExpr -> IntExpr [ditto] .
op _<_ : IntExpr IntExpr -> BoolExpr [ditto] .
op _<=_ : IntExpr IntExpr -> BoolExpr [ditto] .
op _>_ : IntExpr IntExpr -> BoolExpr [ditto].
op _>=_ : IntExpr IntExpr -> BoolExpr [ditto] .
op _===_ : IntExpr IntExpr -> BoolExpr [comm prec 51] .
op _=/==_ : IntExpr IntExpr -> BoolExpr [comm prec 51] .
op _?_:_ : BoolExpr IntExpr IntExpr -> IntExpr [gather (e e e) prec 71] .
--- The following operators are currently not supported.
---(
op _div_ : IntExpr IntExpr -> IntExpr [gather (E e) prec 31] .
op _mod_ : IntExpr IntExpr -> IntExpr [gather (E e) prec 31] .
op _divisible_ : IntExpr IntExpr -> BoolExpr [prec 51] .
---)
vars A B : IntExpr .
vars I J : Int .
--- some basic equations
--- eq A === A = true .
--- eq A <= A = true .
--- eq A >= A = true .
eq (A === B) = A <= B and A >= B .
eq (A =/== B) = A < B or A > B .
eq true ? A : B = A .
eq false ? A : B = B .
endfm
--- Because RAT includes INT, ALT-REAL must include ALT-INTEGER.
fmod ALT-REAL-INTEGER-EXPR is
including VAR-ID .
protecting ALT-INTEGER-EXPR .
including RAT .
sort RExpr .
subsort Rat < RExpr .
sort RVar StRExpr .
subsort RVar < StRExpr < RExpr .
op rr : SMTVarId -> RVar [ctor] .
op -_ : RExpr -> RExpr [ditto] .
op _+_ : RExpr RExpr -> RExpr [ditto] .
op _*_ : RExpr RExpr -> RExpr [ditto] .
op _-_ : RExpr RExpr -> RExpr [ditto] .
op _/_ : RExpr RExpr -> RExpr [ditto] .
op -_ : StRExpr -> StRExpr [ditto] .
op _+_ : StRExpr RExpr -> StRExpr [ditto] .
op _*_ : StRExpr RExpr -> StRExpr [ditto] .
op _-_ : StRExpr RExpr -> StRExpr [ditto] .
op _-_ : RExpr StRExpr -> StRExpr [ditto] .
op _/_ : StRExpr RExpr -> StRExpr [ditto] .
op _/_ : RExpr StRExpr -> StRExpr [ditto] .
op _<_ : RExpr RExpr -> BoolExpr [ditto] .
op _<=_ : RExpr RExpr -> BoolExpr [ditto] .
op _>_ : RExpr RExpr -> BoolExpr [ditto] .
op _>=_ : RExpr RExpr -> BoolExpr [ditto] .
op _===_ : RExpr RExpr -> BoolExpr [comm prec 51] .
op _=/==_ : RExpr RExpr -> BoolExpr [comm prec 51] .
op _?_:_ : BoolExpr RExpr RExpr -> RExpr [gather (e e e) prec 71] .
op _?_:_ : BoolExpr Int Int -> Int [ditto] .
op toReal : IntExpr -> RExpr .
op toInteger : RExpr -> IntExpr .
op isInteger : RExpr -> BoolExpr .
vars A B : RExpr .
var I : Int .
vars R S : Rat .
--- some basic equations
--- eq A === A = true .
--- eq A <= A = true .
--- eq A >= A = true .
eq (A === B) = A <= B and A >= B .
eq (A =/== B) = A < B or A > B .
eq true ? A : B = A .
eq false ? A : B = B .
eq 0 + A = A .
eq toReal(I) = I .
eq toInteger(R) = floor(R) .
eq isInteger(I) = true .
eq isInteger(R) = floor(R) === R .
endfm
--- from an old version of the HybridSynchAADL implementation
fmod META-SMT-CONSTANT-TRANS is
protecting META-LEVEL .
protecting CONVERSION .
vars T T' : Term .
sort Nat? .
subsort Nat < Nat? .
op error : -> Nat? [ctor] .
op metaTrIntC : Term -> TermQid [memo] .
eq metaTrIntC(T) = qid(string(downTerm(T,error),10) + ".Integer") .
op metaTrRatC : Term -> TermQid [memo] .
eq metaTrRatC('_/_[T,T'])
= qid(string(downTerm(T,error),10) + "/" + string(downTerm(T',error),10) + ".Real") .
eq metaTrRatC(T) = qid(string(downTerm(T,error),10) + "/1.Real") [owise] .
endfm
--- translate ALT-SMT exps to SMT exps
fmod SMT-EXP-TRANS is
protecting REAL-INTEGER-EXPR .
protecting ALT-REAL-INTEGER-EXPR .
protecting META-SMT-CONSTANT-TRANS * (op __ to _#_) . --- to avoid a parsing error
op trBool : BoolExpr ~> BooleanExpr .
op trInt : IntExpr ~> IntegerExpr .
op trReal : RExpr ~> RealExpr .
var B : Bool .
var I : Int .
var R : Rat .
var ID : SMTVarId .
vars BE BE1 BE2 : BoolExpr .
vars IE IE1 IE2 : IntExpr .
vars RE RE1 RE2 : RExpr .
--- error terms for downTerm
sort Integer? Real? .
subsort Integer < Integer? .
subsort Real < Real? .
op error : -> Integer? [ctor] .
op error : -> Real? [ctor] .
--- translation for atoms
op trRealAtom : Rat ~> Real [memo].
eq trRealAtom(R) = downTerm(metaTrRatC(upTerm(R)),error) .
op trIntAtom : Int ~> Integer [memo] .
eq trIntAtom(I) = downTerm(metaTrIntC(upTerm(I)),error) .
--- Boolean
eq trBool(true) = true .
eq trBool(false) = false .
eq trBool(bb(ID)) = b(ID) .
eq trBool(not BE) = not trBool(BE) .
eq trBool(BE1 and BE2) = trBool(BE1) and trBool(BE2) .
eq trBool(BE1 xor BE2) = trBool(BE1) xor trBool(BE2) .
eq trBool(BE1 or BE2) = trBool(BE1) or trBool(BE2) .
eq trBool(BE1 implies BE2) = trBool(BE1) implies trBool(BE2) .
eq trBool(BE1 === BE2) = trBool(BE1) === trBool(BE2) .
eq trBool(BE1 =/== BE2) = trBool(BE1) =/== trBool(BE2) .
eq trBool(BE ? BE1 : BE2) = trBool(BE) ? trBool(BE1) : trBool(BE2) .
--- Integer
eq trInt(I) = trIntAtom(I) .
eq trInt(ii(ID)) = i(ID) .
eq trInt(- IE) = - trInt(IE) .
eq trInt(IE1 + IE2) = trInt(IE1) + trInt(IE2) .
eq trInt(IE1 * IE2) = trInt(IE1) * trInt(IE2) .
eq trInt(IE1 - IE2) = trInt(IE1) - trInt(IE2) .
eq trBool(IE1 < IE2) = trInt(IE1) < trInt(IE2) .
eq trBool(IE1 <= IE2) = trInt(IE1) <= trInt(IE2) .
eq trBool(IE1 > IE2) = trInt(IE1) > trInt(IE2) .
eq trBool(IE1 >= IE2) = trInt(IE1) >= trInt(IE2) .
eq trBool(IE1 === IE2) = trInt(IE1) === trInt(IE2) .
eq trBool(IE1 =/== IE2) = trInt(IE1) =/== trInt(IE2) .
eq trInt(BE ? IE1 : IE2) = trBool(BE) ? trInt(IE1) : trInt(IE2) .
--- Real
eq trReal(R) = trRealAtom(R) .
eq trReal(rr(ID)) = r(ID) .
eq trReal(- RE) = - trReal(RE) .
eq trReal(RE1 + RE2) = trReal(RE1) + trReal(RE2) .
eq trReal(RE1 * RE2) = trReal(RE1) * trReal(RE2) .
eq trReal(RE1 - RE2) = trReal(RE1) - trReal(RE2) .
eq trReal(RE1 / RE2) = trReal(RE1) / trReal(RE2) .
eq trBool(RE1 < RE2) = trReal(RE1) < trReal(RE2) .
eq trBool(RE1 <= RE2) = trReal(RE1) <= trReal(RE2) .
eq trBool(RE1 > RE2) = trReal(RE1) > trReal(RE2) .
eq trBool(RE1 >= RE2) = trReal(RE1) >= trReal(RE2) .
eq trBool(RE1 === RE2) = trReal(RE1) === trReal(RE2) .
eq trBool(RE1 =/== RE2) = trReal(RE1) =/== trReal(RE2) .
eq trReal(BE ? RE1 : RE2) = trBool(BE) ? trReal(RE1) : trReal(RE2) .
eq trReal(toReal(IE)) = toReal(trInt(IE)) .
eq trInt(toInteger(RE)) = toInteger(trReal(RE)) .
eq trBool(isInteger(RE)) = isInteger(trReal(RE)) .
endfm
fmod ALT-SMT-CHECK is
protecting SMT-EXP-TRANS .
protecting SMT-CHECK .
var B : Bool . var BE : BoolExpr .
op smtCheck : BoolExpr -> SmtCheckResult .
eq smtCheck(BE) = smtCheck(BE, false) .
op smtCheck : BoolExpr Bool -> SmtCheckResult .
eq smtCheck((true).BoolExpr, B) = true .
eq smtCheck((false).BoolExpr, B) = false .
eq smtCheck(BE, B) = smtCheck(trBool(BE), B) [owise] .
endfm
eof
fmod TEST-TR is
including SMT-EXP-TRANS .
subsort Nat < SMTVarId .
endfm
red trBool(bb(0) and (3 * toInteger(4) > (isInteger(rr(1)) ? toInteger(rr(1)) : 0))) .
red trBool((3/2 * 4/1 > (rr(1) >= 0 ? rr(1) : - rr(1))) implies false) .
fmod TEST-CHECK is
including ALT-SMT-CHECK .
subsort Nat < SMTVarId .
endfm
red smtCheck((3/2 * 4/1 > (rr(1) >= 0 ? rr(1) : - rr(1))) implies false) .
red smtCheck((3/2 * 4/1 > (rr(1) >= 0 ? rr(1) : - rr(1))) implies false, true) .
red smtCheck(rr(2) === (rr(1) > 0 ? rr(1) : - rr(1)) and rr(1) < 0 and rr(2) < 0) .
maude/analysis.maude 0 → 100644
+ 314
− 0
View file @ bca957fc
***(
Some useful commands for parameter synthesis, reachability with folding, etc
TODO
1. In Synthesis, use SET{BoolExpr}
*)
load ./semantics .
--- Some auxiliary definitions for the meta-level
fmod EXT-META-LEVEL is
pr STATE .
--- -------------
vars N N' : Nat .
var MOD : Module .
var ST : State .
var Q : Qid .
var TERM : Term .
var CONS : BoolExpr .
var BOUND : Bound .
--- -------------
--- N steps of rewriting
op one-step : Module State -> State .
op n-steps : Nat Module State -> State .
eq n-steps(N,MOD, ST) = downTerm(getTerm(metaRewrite(MOD, upTerm(ST), N)), (error).State) .
eq one-step(MOD, ST) = n-steps(1, MOD, ST) .
--- Extending the user module with the rules
--- 0: Standard semantics
--- 1: FME simplification at [local] and [binary] steps (DEFAULT)
op module : Nat Qid -> Module .
eq module(N, Q) =
(mod 'NET-ANALYSIS is
including Q . # extending (if N == 0 then 'NPTAD-INTERPRETER else 'NPTAD-INTERPRETER-FME fi) .
sorts none .
none none none none none endm) .
op module : Qid -> Module .
eq module(Q) = module(1, Q) .
--- The Nat parameter is only for printing solutions
--- Return the constraint eliminating the tick variables
op getConstraint : Nat Term -> BoolExpr .
ceq getConstraint(N, TERM) = CONS
if CONS := elim-ticks(getConstraint(downTerm(TERM, (error).State)))
[print "Solution " N ": " CONS] .
op dec : Bound Nat -> Bound .
op dec : Bound -> Bound .
eq dec(BOUND) = dec(BOUND, 2) .
eq dec(unbounded, N) = unbounded .
eq dec(N', N) = if N' > N then sd(N', N) else 0 fi .
--- State from a (meta) term
op getState : Term -> State .
eq getState(TERM) = downTerm(TERM, (error).State) .
endfm
fmod SYNTHESIS is
pr EXT-META-LEVEL .
--- Solutions as sets of constraints
sort SetConstraints .
subsort BoolExpr < SetConstraints .
op nil : -> SetConstraints .
op _,_ : SetConstraints SetConstraints -> SetConstraints [ctor assoc comm id: nil format(d d n o)] .
eq C, C = C .
--- ---------------------------------
vars C C' : BoolExpr .
var N : Nat .
var LOCS : SetLocValuation .
var NET : Network .
var NSOL DEPTH : Nat .
var BSOL BDEPTH : Bound .
var MOD : Module .
var ST : State .
var G : Constraint .
var RES? : ResultTriple? .
var COND : Condition .
vars SCON SCON' : SetConstraints .
--- ---------------------------------
--- Meta-search procedure for synthesis
op search : Nat Bound Bound Module State SetLocValuation Constraint -> SetConstraints .
ceq search(N, BSOL, BDEPTH, MOD, ST, LOCS, G) =
if RES? == failure then nil
else getConstraint(N + 1 , getTerm(RES?)),
(if BSOL == unbounded or-else N + 1 < BSOL then search(N + 1, BSOL, BDEPTH, MOD, ST, LOCS, G) else nil fi)
fi
if COND := if G == true then nil else 'smtCheck['_and_['C:BoolExpr, 'eval[upTerm(G),'CLOCKS:SetClockValuation,'PARAMS:SetParValuation,'DVARS:SetDVarValuation]]] = 'true.Bool fi /\
RES? := metaSearch(MOD,
upTerm(ST),
'`{_`}_['NET:Network,'<`tick:_locs:_clocks:_parameters:_dvariables:_constraint:_n:_>['tickNotOk.TickState, 'LOCS:SetLocValuation,'CLOCKS:SetClockValuation,'PARAMS:SetParValuation,'DVARS:SetDVarValuation,'C:BoolExpr,'N:Nat]] ,
'_subset_[upTerm(LOCS), 'LOCS:SetLocValuation ] = 'true.Bool /\ COND,
'*,
BDEPTH,
N) .
--- Checking if C implies C'
op entails : BoolExpr BoolExpr -> Bool .
eq entails(C, C') = not smtCheck(not (C implies C')) .
endfm
--- Adding a constructor for shared states with less information
fmod ALT-SHARED-STATE is
pr SYNTHESIS .
op < locs:_ dvariables:_ > : SetLocValuation SetDVarValuation -> SharedState [ctor] .
op < locs:_ dvariables:_ constraint:_ > : SetLocValuation SetDVarValuation BoolExpr -> SharedState [ctor] .
endfm
view SharedState from TRIV to ALT-SHARED-STATE is sort Elt to SharedState . endv
view BoolExprView from TRIV to ALT-BOOLEAN-EXPR is sort Elt to BoolExpr . endv
fmod FOLDING is
pr SYNTHESIS .
--- A Map from < loc, dvars> to disjunctions of BoolExpr
pr MAP{ SharedState, BoolExprView } * ( sort Entry{SharedState, BoolExprView} to Key,
sort Map{SharedState, BoolExprView} to Map) .
pr SET{SharedState} * (sort Set{SharedState} to SetSharedState, sort NeSet{LocVal} to NeSetSharedState) .
sorts FilterResult FoldingResult .
op <_,_,_> : Map SetSharedState Nat -> FilterResult [ctor] .
op <_,_> : Map Bool -> FoldingResult [ctor] .
--- ---------------------------
var BDEPTH : Bound .
var BSOL : Bound .
vars MAP MAP' : Map .
vars FRONTIER FRONTIER' : SetSharedState .
var NEXT : SetSharedState .
var S : State .
var MOD : Module .
vars LOCS LOCS' : SetLocValuation .
var NET : Network .
vars ST ST' : SharedState .
vars CONS CONS' : BoolExpr .
var CONS? : [BoolExpr] .
var CLOCK : Clock .
var CVALUES : SetClockValuation .
var TS : TickState .
var DVARS : SetDVarValuation .
var PARAMS : SetParValuation .
var RE1 : RExpr .
vars N NSOL : Nat .
var RES? : ResultTriple? .
var SOL-FOUND SOL-FOUND' : Bool .
var G : Constraint .
vars SCON : SetConstraints .
--- ---------------------------
--- Folding procedure
op folding : Bound Bound Module State SetLocValuation Constraint -> FoldingResult .
op folding : Bound Bound Module Network SetLocValuation Constraint Map SetSharedState Bool -> FoldingResult .
eq folding(BSOL, BDEPTH, MOD, S, LOCS, G) =
folding(BSOL, BDEPTH, MOD, get-network(S), LOCS, G, empty, get-state(S), false) .
ceq folding(BSOL, BDEPTH , MOD, NET, LOCS, G, MAP, FRONTIER, SOL-FOUND) =
< MAP , SOL-FOUND or (LOCS == empty and G == true) >
if BSOL == 0 or-else BDEPTH == 0 or-else FRONTIER == empty .
ceq folding(BSOL, BDEPTH, MOD, NET, LOCS, G, MAP, FRONTIER, SOL-FOUND) =
folding(dec(BSOL, NSOL), dec(BDEPTH), MOD, NET, LOCS, G, MAP', NEXT, (SOL-FOUND or NSOL > 0))
if < MAP', FRONTIER', NSOL > := filter(MOD, LOCS, G, MAP, FRONTIER) /\
NEXT := next(MOD, NET, FRONTIER')
[owise] .
--- Filtering already seen solutions
op filter : Module SetLocValuation Constraint Map SetSharedState -> FilterResult .
op $filter : Module SetLocValuation Constraint Map SetSharedState SetSharedState Nat -> FilterResult .
eq filter(MOD, LOCS, G, MAP, FRONTIER) = $filter(MOD, LOCS, G, MAP, FRONTIER, empty, 0) .
eq $filter(MOD, LOCS, G, MAP, empty, FRONTIER', NSOL) = < MAP , FRONTIER', NSOL > .
ceq $filter(MOD, LOCS, G, MAP, (ST, FRONTIER), FRONTIER', NSOL) =
if subsumed?(ST', MAP)
then $filter(MOD, LOCS, G, MAP, FRONTIER, FRONTIER', NSOL)
else $filter(MOD, LOCS, G, add(MAP, ST'), FRONTIER, (ST, FRONTIER'),
NSOL + if isSolution(ST, LOCS, G) then 1 else 0 fi )
fi
if ST' := no-ticks(ST) .
--- Some extra operations on SharedState
op no-ticks : SharedState -> SharedState .
eq no-ticks(< tick: TS locs: LOCS clocks: CVALUES parameters: PARAMS dvariables: DVARS constraint: CONS n: N >) =
< locs: LOCS dvariables: DVARS constraint: elim-ticks(CONS and to-vars-clock-C(CVALUES)) > .
--- "replacing" the current value of the clock with rr(var(CLOCK))
op to-vars-clock-C : SetClockValuation -> BoolExpr .
eq to-vars-clock-C (empty) = true .
eq to-vars-clock-C ((CLOCK : RE1, CVALUES)) = (rr(var(CLOCK)) === RE1) and to-vars-clock-C(CVALUES) .
--- Updating the map with already seen states
op add : Map SharedState -> Map .
eq add((MAP , < locs: LOCS dvariables: DVARS > |-> CONS ),
< locs: LOCS dvariables: DVARS constraint: CONS' > ) =
MAP, < locs: LOCS dvariables: DVARS > |-> (CONS or CONS') .
eq add(MAP , < locs: LOCS dvariables: DVARS constraint: CONS' > ) =
MAP, < locs: LOCS dvariables: DVARS > |-> CONS' [owise] .
--- Checking if a state is a solution
op isSolution : SharedState SetLocValuation Constraint -> Bool .
eq isSolution(< tick: TS locs: LOCS clocks: CVALUES parameters: PARAMS dvariables: DVARS constraint: CONS n: N >,
LOCS', G) =
not( LOCS' == empty and G == true) and-then --- trivial queries are not considered solutions
( LOCS' == empty or-else LOCS' subset LOCS) and-then
( G == true or-else smtCheck(CONS and eval(G, CVALUES, PARAMS, DVARS))) .
--- Checking subsumption: the new state implies the disjunction of the
--- already seen states
op subsumed? : SharedState Map -> Bool .
ceq subsumed?( < locs: LOCS dvariables: DVARS constraint: CONS >, MAP ) =
CONS? =/= undefined and-then not smtCheck(not (CONS implies CONS?))
if CONS? := MAP[ < locs: LOCS dvariables: DVARS > ] .
--- Next frontier
op next : Module Network SetSharedState -> SetSharedState .
op $next : Module Network SetSharedState SetSharedState -> SetSharedState .
op $next : Nat Module Network SharedState SetSharedState -> SetSharedState .
eq next(MOD, NET, FRONTIER) = $next(MOD, NET, FRONTIER, empty) . --- [print "NEXT"] .
eq $next(MOD, NET, empty, FRONTIER') = FRONTIER' .
eq $next(MOD, NET, (ST, FRONTIER), FRONTIER') =
$next(MOD, NET, FRONTIER, (FRONTIER', $next(0, MOD, NET, ST, empty))) .
ceq $next(N, MOD, NET, ST, FRONTIER) =
if RES? == failure then FRONTIER
else $next(N + 1, MOD, NET, ST, (get-state(getState(getTerm(RES?))), FRONTIER))
fi
if RES? := metaSearch(MOD,
upTerm(make-state(NET, ST)),
'`{_`}_['NET:Network,'<`tick:_locs:_clocks:_parameters:_dvariables:_constraint:_n:_>['tickNotOk.TickState, 'LOCS:SetLocValuation,'CLOCKS:SetClockValuation,'PARAMS:SetParValuation,'DVARS:SetDVarValuation,'C:BoolExpr,'N:Nat]] ,
nil,
'+,
2, --- Depth 2: rule + tick
N) .
op getSolutions : FoldingResult SetLocValuation -> SetConstraints .
op getSolutions : Map SetLocValuation SetConstraints -> SetConstraints .
eq getSolutions( < MAP, false >, LOCS) = nil .
eq getSolutions( < MAP, true >, LOCS) = getSolutions(MAP, LOCS, nil) .
eq getSolutions(empty, LOCS, SCON) = SCON .
eq getSolutions( (MAP, < locs: LOCS' dvariables: DVARS > |-> CONS ), LOCS, SCON) = getSolutions(MAP, LOCS, (SCON, if LOCS subset LOCS' then to-set(CONS) else nil fi) ) .
--- From a disjunction of constraints to a set of constraints and eliminating clock variables
op to-set : BoolExpr -> SetConstraints .
eq to-set(CONS or CONS') = to-set(CONS), to-set(CONS') .
eq to-set(CONS) = elim-clocks(CONS) [owise] .
endfm
--- Commands for analysis
fmod ANALYSIS is
pr FOLDING .
--- ----------------------------
var S : State .
var Q : Qid .
var LOCS : SetLocValuation .
var NSOL DEPTH : Nat .
var BSOL BDEPTH : Bound .
var G : Constraint .
--- ----------------------------
--- Synthesis for the EF(loc) problem
op synthesis in _:_=>_ : Qid State NeSetLocValuation -> SetConstraints .
op synthesis `[_`] in_:_=>_ : Nat Qid State NeSetLocValuation -> SetConstraints .
op synthesis `[;_`] in_:_=>_ : Nat Qid State NeSetLocValuation -> SetConstraints .
op synthesis `[_;_`] in_:_=>_ : Nat Nat Qid State NeSetLocValuation -> SetConstraints .
op synthesis in _:_=>_ such that_ : Qid State NeSetLocValuation Constraint -> SetConstraints .
op synthesis `[_`] in_:_=>_ such that_ : Nat Qid State NeSetLocValuation Constraint -> SetConstraints .
op synthesis `[;_`] in_:_=>_ such that_ : Nat Qid State NeSetLocValuation Constraint -> SetConstraints .
op synthesis `[_;_`] in_:_=>_ such that_ : Nat Nat Qid State NeSetLocValuation Constraint -> SetConstraints .
eq synthesis in Q : S => LOCS = search(0, unbounded, unbounded, module(Q), S, LOCS, true) .
eq synthesis [ NSOL ] in Q : S => LOCS = search(0, NSOL, unbounded, module(Q), S, LOCS, true) .
eq synthesis [ ; DEPTH ] in Q : S => LOCS = search(0, unbounded, DEPTH, module(Q), S, LOCS, true) .
eq synthesis [ NSOL ; DEPTH ] in Q : S => LOCS = search(0, NSOL, DEPTH, module(Q), S, LOCS, true) .
eq synthesis in Q : S => LOCS such that G = search(0, unbounded, unbounded, module(Q), S, LOCS, G) .
eq synthesis [ NSOL ] in Q : S => LOCS such that G = search(0, NSOL, unbounded, module(1 ,Q), S, LOCS, G) .
eq synthesis [ ; DEPTH ] in Q : S => LOCS such that G = search(0, unbounded, DEPTH, module(Q), S, LOCS, G) .
eq synthesis [ NSOL ; DEPTH ] in Q : S => LOCS such that G = search(0, NSOL, DEPTH, module(Q), S, LOCS, G) .
op search-folding in _:_=>_ : Qid State NeSetLocValuation -> FoldingResult .
op search-folding in _:_ : Qid State -> FoldingResult .
op search-folding `[_`] in_:_=>_ : Nat Qid State NeSetLocValuation -> FoldingResult .
op search-folding `[;_`] in_:_=>_ : Nat Qid State NeSetLocValuation -> FoldingResult .
op search-folding `[_;_`] in_:_=>_ : Nat Nat Qid State NeSetLocValuation -> FoldingResult .
op search-folding in _:_=>_ such that_ : Qid State NeSetLocValuation Constraint -> FoldingResult .
op search-folding `[_`] in_:_=>_ such that_ : Nat Qid State NeSetLocValuation Constraint -> FoldingResult .
op search-folding `[;_`] in_:_=>_ such that_ : Nat Qid State NeSetLocValuation Constraint -> FoldingResult .
op search-folding `[_;_`] in_:_=>_ such that_ : Nat Nat Qid State NeSetLocValuation Constraint -> FoldingResult .
op synthesis-folding in_:_=>_ : Qid State NeSetLocValuation -> SetConstraints .
eq search-folding in Q : S = folding(unbounded, unbounded, module(Q), one-step(module(Q), S), empty, true) .
eq search-folding in Q : S => LOCS = folding(unbounded, unbounded, module(Q), one-step(module(Q), S), LOCS, true) .
eq search-folding [ NSOL ] in Q : S => LOCS = folding(NSOL, unbounded, module(Q), one-step(module(Q), S), LOCS, true) .
eq search-folding [ ; DEPTH ] in Q : S => LOCS = folding(unbounded, DEPTH, module(Q), one-step(module(Q), S), LOCS, true) .
eq search-folding [ NSOL ; DEPTH ] in Q : S => LOCS = folding(NSOL, DEPTH, module(Q), one-step(module(Q), S), LOCS, true) .
eq search-folding in Q : S => LOCS such that G = folding(unbounded, unbounded, module(Q), one-step(module(Q), S), LOCS, G) .
eq search-folding [ NSOL ] in Q : S => LOCS such that G = folding(NSOL, unbounded, module(1 ,Q), one-step(module(Q), S), LOCS, G) .
eq search-folding [ ; DEPTH ] in Q : S => LOCS such that G = folding(unbounded, DEPTH, module(Q), one-step(module(Q), S), LOCS, G) .
eq search-folding [ NSOL ; DEPTH ] in Q : S => LOCS such that G = folding(NSOL, DEPTH, module(Q), one-step(module(Q), S), LOCS, G) .
eq synthesis-folding in Q : S => LOCS = getSolutions(folding(unbounded, unbounded, module(Q), one-step(module(Q), S), LOCS, true), LOCS) .
endfm
maude/examples/checking-train-solutions.maude 0 → 100644
+ 284
− 0
View file @ bca957fc
Source diff could not be displayed: it is too large. Options to address this: view the blob.
maude/examples/coffee-folding.maude deleted 100644 → 0
+ 0
− 80
View file @ a56eab5a
***(
Coffee Machine
--------------
In the command below, we show that adding the constraint 2/1 * P1 > P2
makes the transition finite
*)
load pta-base .
mod MODEL is
inc MODEL-BASE .
pr REAL .
--- --------------------------
vars X1 X2 : Real .
vars X1' X2' : Real .
vars P1 P2 P3 : Real .
var T : Real .
var L : Location .
--- --------------------------
ops idle sugar coffee done : -> Location .
op <_:_;_> <_;_;_> : Location Real Real Real Real Real -> NState .
op [_:_;_] <_;_;_> : Location Real Real Real Real Real -> DState .
crl [idle-sugar] : < idle : X1 ; X2 > < P1 ; P2 ; P3 > =>
[ sugar : 0/1 ; 0/1 ] < P1 ; P2 ; P3 >
if (0/1 <= P2) = true [nonexec] .
crl [tick-idle] : [ idle : X1 ; X2 ] < P1 ; P2 ; P3 > =>
< idle : X1 + T ; X2 + T > < P1 ; P2 ; P3 >
if (T >= 0/1) = true [nonexec] .
crl [sugar-sugar] : < sugar : X1 ; X2 > < P1 ; P2 ; P3 > =>
[ sugar : 0/1 ; X2 ] < P1 ; P2 ; P3 >
if (X2 <= P2 and X1 >= P1) = true [nonexec] .
crl [sugar-coffee] : < sugar : X1 ; X2 > < P1 ; P2 ; P3 > =>
[ coffee : X1 ; X2 ] < P1 ; P2 ; P3 >
if (X2 <= P3 and X2 === P2) = true .
crl [tick-sugar] : [ sugar : X1 ; X2 ] < P1 ; P2 ; P3 > =>
< sugar : X1 + T ; X2 + T > < P1 ; P2 ; P3 >
if (T >= 0/1 and X2 + T <= P2) = true [nonexec] .
crl [coffee-done] : < coffee : X1 ; X2 > < P1 ; P2 ; P3 > =>
[ done : 0/1 ; X2 ] < P1 ; P2 ; P3 >
if (0/1 <= 10/1 and X2 === P3) = true [nonexec] .
crl [tick-coffee] : [ coffee : X1 ; X2 ] < P1 ; P2 ; P3 > =>
< coffee : X1 + T ; X2 + T > < P1 ; P2 ; P3 >
if (T >= 0/1 and X2 + T <= P3) = true [nonexec] .
crl [done-sugar] : < done : X1 ; X2 > < P1 ; P2 ; P3 > =>
[ sugar : 0/1 ; 0/1 ] < P1 ; P2 ; P3 >
if (0/1 <= P2) = true [nonexec] .
crl [done-idle] : < done : X1 ; X2 > < P1 ; P2 ; P3 > =>
[ idle : X1 ; X2 ] < P1 ; P2 ; P3 >
if (X1 === 10/1) = true [nonexec] .
crl [tick-done] : [ done : X1 ; X2 ] < P1 ; P2 ; P3 > =>
< done : X1 + T ; X2 + T > < P1 ; P2 ; P3 >
if (T >= 0/1 and X1 + T <= 10/1) = true [nonexec] .
eq get-location( < L : X1 ; X2 > < P1 ; P2 ; P3 > ) = L .
eq get-location( [ L : X1 ; X2 ] < P1 ; P2 ; P3 > ) = L .
endm
load meta-pta .
red reachability( (< idle : T:Real ; T:Real > < P1:Real ; P2:Real ; P3:Real >
| T:Real >= 0/1 and P1:Real >= 0/1 and P2:Real >= 0/1 and P3:Real >= 0/1 and
2/1 * P1:Real > P2:Real)) .
maude/examples/coffee-strategy.maude
+ 52
− 167
View file @ bca957fc
......@@ -6,192 +6,77 @@
It must be run with Maude SE https://maude-se.github.io/
*)
load smt
load smt-check
mod PTA-COFFEE is
pr SMT-CHECK .
inc NAT .
pr QID .
--- Fresh variables
subsort Nat < SMTVarId .
subsort Qid < SMTVarId .
--- ---------------------------
vars x y z : RealExpr .
vars x' y' z' : RealExpr .
vars p1 p2 p3 : RealExpr .
var t : RealExpr .
var N : Nat .
vars C C' : BooleanExpr .
--- ---------------------------
sorts State State' Location .
--- Global configuration
op <_|_|_> : Nat BooleanExpr State' -> State .
--- Configurations
ops idle sugar coffee done : -> Location .
op <_;_;_> <_;_;_> : Location RealExpr RealExpr RealExpr RealExpr RealExpr -> State' .
op [_;_;_] <_;_;_> : Location RealExpr RealExpr RealExpr RealExpr RealExpr -> State' .
crl [press] :
< N | C | < idle ; x ; y > < p1 ; p2 ; p3 > > =>
< N | C' | [ sugar ; 0/1 ; 0/1 ] < p1 ; p2 ; p3 > >
if
C' := simplify(C and 0/1 <= p2) /\
smtCheck(C')
.
crl [tick-idle] :
< N | C | [ idle ; x ; y ] < p1 ; p2 ; p3 > > =>
< N + 1 | C' | < idle ; x + t ; y + t > < p1 ; p2 ; p3 > >
if
t := r(N) /\
C' := simplify(C and t >= 0/1) /\
smtCheck(C')
.
crl [sugar] :
< N | C | < sugar ; x ; y > < p1 ; p2 ; p3 > > =>
< N | C' | [ sugar ; 0/1 ; y ] < p1 ; p2 ; p3 > >
if
C' := simplify(C and x >= p1 and y <= p2) /\
smtCheck(C')
.
crl [tick-sugar] :
< N | C | [ sugar ; x ; y ] < p1 ; p2 ; p3 > > =>
< N + 1 | C' | < sugar ; x + t ; y + t > < p1 ; p2 ; p3 > >
if
t := r(N) /\
C' := simplify(C and (y + t <= p2 and t >= 0/1)) /\
smtCheck(C')
.
crl [cup] :
< N | C | < sugar ; x ; y > < p1 ; p2 ; p3 > > =>
< N | C' | [ coffee ; x ; y ] < p1 ; p2 ; p3 > >
if
C' := simplify(C and (y === p2 and y <= p3 )) /\
smtCheck(C')
.
crl [tick-coffee] :
< N | C | [ coffee ; x ; y ] < p1 ; p2 ; p3 > > =>
< N + 1 | C' | < coffee ; x + t ; y + t > < p1 ; p2 ; p3 > >
if
t := r(N) /\
C' := simplify(C and (t >= 0/1 and y + t <= p3)) /\
smtCheck(C')
.
crl [coffee] :
< N | C | < coffee ; x ; y > < p1 ; p2 ; p3 > > =>
< N | C' | [ done ; 0/1 ; y ] < p1 ; p2 ; p3 > >
if
C' := simplify(C and (y === p3 )) /\
smtCheck(C')
.
crl [done] :
< N | C | < done ; x ; y > < p1 ; p2 ; p3 > > =>
< N | C' | [ idle ; x ; y ] < p1 ; p2 ; p3 > >
if
C' := simplify(C and (x === 10/1 )) /\
smtCheck(C')
.
crl [tick-done] :
< N | C | [ done ; x ; y ] < p1 ; p2 ; p3 > > =>
< N + 1 | C' | < done ; x + t ; y + t > < p1 ; p2 ; p3 > >
if
t := r(N) /\
C' := simplify(C and (t >= 0/1 and x + t <= 10/1)) /\
smtCheck(C')
.
rl [done] :
< N | C | < done ; x ; y > < p1 ; p2 ; p3 > > =>
< N | C | [ sugar ; 0/1 ; 0/1 ] < p1 ; p2 ; p3 > >
.
--- simplifyFormula can be used here instead
op simplify : BooleanExpr -> BooleanExpr .
eq simplify(C) = C .
load ../analysis .
mod COFFEE is
extending NPAD-INTERPRETER .
ops idle addsugar preparing done : -> Location [ctor] .
ops bstart bsugar cup coffee sleep : -> Action [ctor] .
ops coffee : -> Agent [ctor] .
ops x1 x2 : -> Clock [ctor] .
ops p1 p2 p3 : -> Parameter [ctor] .
op coffee : -> Automaton .
eq coffee = < coffee | (@ idle inv true :
(when true local bstart do {x1 := 0 ; x2 := 0} goto addsugar)),
(@ addsugar inv x2 <= p2 :
(when x1 >= p1 local bsugar do {x1 := 0} goto addsugar ,
when x2 = p2 local cup goto preparing)),
(@ preparing inv x2 <= p3 :
(when x2 = p3 local coffee do {x1 := 0} goto done)) ,
(@ done inv x1 <= 10 :
(when x1 = 10 local sleep goto idle ,
when true local bstart do { x1 := 0 ; x2 := 0 } goto addsugar))
> .
op init : -> State .
eq init = {coffee}
< tick: tickOk
locs: coffee @ idle
clocks: (x1 : 0, x2 : 0)
parameters: (p1 : rr(var(p1)), p2 : rr(var(p2)), p3 : rr(var(p3)))
dvariables: empty
constraint: rr(var(p1)) >= 0 and rr(var(p2)) >= 0 and rr(var(p3)) >= 0 --- and 2 * rr(var(p1)) > rr(var(p2))
n: 1
>
.
endm
--- Definition of strategies
smod COFFEE-STR is
protecting PTA-COFFEE .
protecting COFFEE .
strat sugar-str : Nat @ State .
strat sugar-str' @ State .
strat withSugar : Nat @ State .
strat add-sugar : Nat @ State .
strat n-coffees : Nat @ State .
strat $n-coffees : Nat @ State .
--- ---------------------------
vars x y z : RealExpr .
vars x' y' z' : RealExpr .
vars p1 p2 p3 : RealExpr .
var t : RealExpr .
var N : Nat .
vars C C' : BooleanExpr .
var CVALUES : SetClockValuation .
var PVALUES : SetParValuation .
var DVVALUES : SetDVarValuation .
var ACT : Action .
var NET : Network .
var CONS : BoolExpr .
vars N N' : Nat .
--- ---------------------------
op validity : BooleanExpr -> SmtCheckResult .
eq validity(C) = smtCheck(not C) == false .
vars S : Nat .
--- Adding S times sugar
sd sugar-str(S) := (match < N | C | [ done ; x ; y ] < p1 ; p2 ; p3 > > ) or-else --- end
(
(match < N | C | < sugar ; x ; y > < p1 ; p2 ; p3 > > ) ; add-sugar(S) ; cup ; sugar-str(S)
) or-else --- adding sugar and delivering coffee
all ; sugar-str(S) .
--- an alternative version using smt calls. Sugar is added only once (when x == y in state sugar)
sd sugar-str' := (match < N | C | [ done ; x ; y ] < p1 ; p2 ; p3 > > ) or-else --- end
(
(match < N | C | < sugar ; x ; y > < p1 ; p2 ; p3 > > s.t. validity( C implies x === y)) ; add-sugar(1) ; cup ; sugar-str'
) or-else --- adding sugar and delivering coffee
all ; sugar-str' .
sd with-sugar(N) :=
(match { NET } < tick: tickNotOk locs: (coffee @ done) clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N' > ) or-else --- end
(match { NET } < tick: tickNotOk locs: (coffee @ addsugar) clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >
s.t. smtCheck( CONS and eval( x1 - x2 = 0, CVALUES, PVALUES, DVVALUES)) ; add-sugar(N) ; local [ ACT <- cup ] ; with-sugar(N)) or-else
all ; with-sugar(N) .
--- Performing the sugar action
sd add-sugar(0) := idle .
sd add-sugar(s(N)) := sugar ; tick-sugar ; add-sugar(N) .
sd add-sugar(s(N)) := local [ ACT <- bsugar ] ; tick ; add-sugar(N) .
--- N coffees with 1 sugar each
sd n-coffees(S) := (match < N | C | [ done ; x ; y ] < p1 ; p2 ; p3 > > ; $n-coffees(S) ) or-else --- end
(
(match < N | C | < sugar ; x ; y > < p1 ; p2 ; p3 > > ) ; add-sugar(1) ; cup ; n-coffees(S)
) or-else --- adding sugar and delivering coffee
all ; n-coffees(S) .
sd $n-coffees(1) := idle .
csd $n-coffees(s(S)) := tick-done ; n-coffees(S) if S =/= 0 .
endsm
--- With 1 sugar, besides p2 <= p3, it must be also the case that p1 <= p2
srew [1] < 0 | (r('p1) >= 0/1 and r('p2) >= 0/1 and r('p3) >= 0/1 ) | [ idle ; 0/1 ; 0/1 ] < r('p1) ; r('p2); r('p3) > >
using sugar-str(1) .
srew [1] < 0 | (r('p1) >= 0/1 and r('p2) >= 0/1 and r('p3) >= 0/1 ) | [ idle ; 0/1 ; 0/1 ] < r('p1) ; r('p2); r('p3) > >
using sugar-str' .
eof
srew [1] < 0 | (r('p1) >= 0/1 and r('p2) >= 0/1 and r('p3) >= 0/1 ) | [ idle ; 0/1 ; 0/1 ] < r('p1) ; r('p2); r('p3) > >
using n-coffees(2) .
srew [1] init using withSugar(1) .
quit .
maude/examples/coffee.maude
+ 47
− 68
View file @ bca957fc
***(
Coffee Machine
--------------
*)
load pta-base .
mod MODEL is
inc MODEL-BASE .
pr REAL .
--- --------------------
vars X1 X2 : Real .
vars X1' X2' : Real .
vars P1 P2 P3 : Real .
var T : Real .
--- --------------------
ops idle sugar coffee done : -> Location .
op <_:_;_> <_;_;_> : Location Real Real Real Real Real -> NState .
op [_:_;_] <_;_;_> : Location Real Real Real Real Real -> DState .
crl [idle-sugar] : < idle : X1 ; X2 > < P1 ; P2 ; P3 > =>
[ sugar : 0/1 ; 0/1 ] < P1 ; P2 ; P3 >
if (0/1 <= P2) = true [nonexec] .
crl [tick-idle] : [ idle : X1 ; X2 ] < P1 ; P2 ; P3 > =>
< idle : X1 + T ; X2 + T > < P1 ; P2 ; P3 >
if (T >= 0/1) = true [nonexec] .
crl [sugar-sugar] : < sugar : X1 ; X2 > < P1 ; P2 ; P3 > =>
[ sugar : 0/1 ; X2 ] < P1 ; P2 ; P3 >
if (X2 <= P2 and X1 >= P1) = true [nonexec] .
crl [sugar-coffee] : < sugar : X1 ; X2 > < P1 ; P2 ; P3 > =>
[ coffee : X1 ; X2 ] < P1 ; P2 ; P3 >
if (X2 <= P3 and X2 === P2) = true .
crl [tick-sugar] : [ sugar : X1 ; X2 ] < P1 ; P2 ; P3 > =>
< sugar : X1 + T ; X2 + T > < P1 ; P2 ; P3 >
if (T >= 0/1 and X2 + T <= P2) = true [nonexec] .
crl [coffee-done] : < coffee : X1 ; X2 > < P1 ; P2 ; P3 > =>
[ done : 0/1 ; X2 ] < P1 ; P2 ; P3 >
if (0/1 <= 10/1 and X2 === P3) = true [nonexec] .
crl [tick-coffee] : [ coffee : X1 ; X2 ] < P1 ; P2 ; P3 > =>
< coffee : X1 + T ; X2 + T > < P1 ; P2 ; P3 >
if (T >= 0/1 and X2 + T <= P3) = true [nonexec] .
crl [done-sugar] : < done : X1 ; X2 > < P1 ; P2 ; P3 > =>
[ sugar : 0/1 ; 0/1 ] < P1 ; P2 ; P3 >
if (0/1 <= P2) = true [nonexec] .
crl [done-idle] : < done : X1 ; X2 > < P1 ; P2 ; P3 > =>
[ idle : X1 ; X2 ] < P1 ; P2 ; P3 >
if (X1 === 10/1) = true [nonexec] .
crl [tick-done] : [ done : X1 ; X2 ] < P1 ; P2 ; P3 > =>
< done : X1 + T ; X2 + T > < P1 ; P2 ; P3 >
if (T >= 0/1 and X1 + T <= 10/1) = true [nonexec] .
--- The example of the coffee machine using the interpreter
load ../analysis .
mod COFFEE is
extending ANALYSIS .
ops idle addsugar preparing done : -> Location [ctor] .
ops bstart bsugar cup coffee sleep : -> Action [ctor] .
ops coffee : -> Agent [ctor] .
ops x1 x2 : -> Clock [ctor] .
ops p1 p2 p3 : -> Parameter [ctor] .
op coffee : -> Automaton .
eq coffee = < coffee | (@ idle inv true :
(when true local bstart do {x1 := 0 ; x2 := 0} goto addsugar)),
(@ addsugar inv x2 <= p2 :
(when x1 >= p1 local bsugar do {x1 := 0} goto addsugar ,
when x2 = p2 local cup goto preparing)),
(@ preparing inv x2 <= p3 :
(when x2 = p3 local coffee do {x1 := 0} goto done)) ,
(@ done inv x1 <= 10 :
(when x1 = 10 local sleep goto idle ,
when true local bstart do { x1 := 0 ; x2 := 0 } goto addsugar))
> .
op init : -> State .
eq init = {coffee}
< tick: tickOk
locs: coffee @ idle
clocks: (x1 : 0, x2 : 0)
parameters: (p1 : rr(var(p1)), p2 : rr(var(p2)), p3 : rr(var(p3)))
dvariables: empty
constraint: rr(var(p1)) >= 0 and rr(var(p2)) >= 0 and rr(var(p3)) >= 0 and 2 * rr(var(p1)) > rr(var(p2))
n: 1
>
.
endm
eof
--- Solving EF(loc = done) --- one solution
red synthesis [ 1 ] in 'COFFEE : init => (coffee @ done) .
red synthesis [ 1 ] in 'COFFEE : init => (coffee @ done) such that ( x2 - x1 > 0 ) .
--- Solving EF(loc=done) with folding
--- This property does not hold
--- This loops
red synthesis [ 1 ; 10 ] in 'COFFEE : init => empty such that ( x1 - x2 > 0 ) .
--- This finishes (with answer no)
red search-folding in 'COFFEE : init => empty such that ( x1 - x2 > 0 ) .
--- Finding whether the location done is reachable
smt-search [1] < idle : X1 ; X2 > < P1 ; P2 ; P3 > =>*
< done : X1' ; X2' > < P1 ; P2 ; P3 >
such that (X1 === X2 and X1 >= 0/1 and
P1 >= 0/1 and P2 >= 0/1 and P3 >= 0/1 ) = true .
maude/examples/ex-fig3a.maude deleted 100644 → 0
+ 0
− 68
View file @ a56eab5a
***(
Infinite states
--------------
Example in Figure 3a (infinite number of states)
The location BAD is reachable in this case
*)
load smt .
mod EXAMPLE-INF is
pr REAL .
sorts State Location .
--- ---------------------------
vars X Y : Real .
vars X' Y' : Real .
vars T : Real .
--- ---------------------------
--- Configurations
ops l0 l1 bad : -> Location .
op <_:_;_> : Location Real Real -> State .
op [_:_;_] : Location Real Real -> State .
crl [l0-l1] :
< l0 : X ; Y > =>
[ l1 : X ; Y ]
if ( 5/1 <= X and 10/1 >= X ) = true .
crl [l0-tick] :
[ l0 : X ; Y ] =>
< l0 : X + T ; Y + T >
if (T >= 0/1) = true [nonexec] .
crl [l1-l0] :
< l1 : X ; Y > =>
[ l0 : 0/1 ; Y ]
if (true) = true .
crl [l1-tick] :
[ l1 : X ; Y ] =>
< l1 : X + T ; Y + T >
if (T >= 0/1 and 10/1 >= X + T) = true [nonexec] .
crl [l1-bad] :
< l1 : X ; Y > =>
[ bad : X ; Y ]
if (X >= 11/1) = true .
crl [l1-bad] :
< l1 : X ; Y > =>
[ bad : X ; Y ]
if (Y >= 50/1) = true .
crl [bad-tick] :
[ bad : X ; Y ] =>
< bad : X + T ; Y + T >
if (T >= 0/1) = true [nonexec] .
endm
smt-search [1] [ l0 : 0/1 ; 0/1 ] =>* [ bad : X' ; Y' ] .
maude/examples/ex-fig3b-folding.maude deleted 100644 → 0
+ 0
− 69
View file @ a56eab5a
***(
Infinite states
--------------
EXample in Figure 3b (infinite number of states)
The location BAD is not reachable
The command reachability finds the only 2 symbolic states in this PTA
*)
load pta-base .
mod MODEL is
inc MODEL-BASE .
pr REAL .
--- ---------------------------
vars X Y : Real .
vars X' Y' : Real .
vars T : Real .
--- ---------------------------
--- Configurations
ops l0 l1 bad : -> Location .
op <_:_> : Location Real -> NState .
op [_:_] : Location Real -> DState .
crl [l0-l1] :
< l0 : X > =>
[ l1 : X ]
if ( 5/1 <= X and 10/1 >= X ) = true .
crl [l0-tick] :
[ l0 : X ] =>
< l0 : X + T >
if (T >= 0/1) = true [nonexec] .
crl [l1-l0] :
< l1 : X > =>
[ l0 : 0/1 ]
if (true) = true .
crl [l1-tick] :
[ l1 : X ] =>
< l1 : X + T >
if (T >= 0/1 and 10/1 >= X + T) = true [nonexec] .
crl [l1-bad] :
< l1 : X > =>
[ bad : X ]
if (X >= 11/1) = true .
crl [bad-tick] :
[ bad : X ] =>
< bad : X + T >
if (T >= 0/1) = true [nonexec] .
endm
load meta-pta .
red reachability( (< l0 : X:Real > | X:Real >= 0/1)) .
maude/examples/ex-fig3b.maude deleted 100644 → 0
+ 0
− 64
View file @ a56eab5a
***(
Infinite states
--------------
EXample in Figure 3b (infinite number of states)
The location BAD is not reachable and the search command loops (see
the bounded limit in the smt-search command below)
*)
load pta-base .
mod MODEL is
inc MODEL-BASE .
pr REAL .
--- ---------------------------
vars X Y : Real .
vars X' Y' : Real .
vars T : Real .
--- ---------------------------
--- Configurations
ops l0 l1 bad : -> Location .
op <_:_> : Location Real -> NState .
op [_:_] : Location Real -> DState .
crl [l0-l1] :
< l0 : X > =>
[ l1 : X ]
if ( 5/1 <= X and 10/1 >= X ) = true .
crl [l0-tick] :
[ l0 : X ] =>
< l0 : X + T >
if (T >= 0/1) = true [nonexec] .
crl [l1-l0] :
< l1 : X > =>
[ l0 : 0/1 ]
if (true) = true .
crl [l1-tick] :
[ l1 : X ] =>
< l1 : X + T >
if (T >= 0/1 and 10/1 >= X + T) = true [nonexec] .
crl [l1-bad] :
< l1 : X > =>
[ bad : X ]
if (X >= 11/1) = true .
crl [bad-tick] :
[ bad : X ] =>
< bad : X + T >
if (T >= 0/1) = true [nonexec] .
endm
--- smt-search bound to 10 steps (otherwise, it does not stop)
smt-search [1,10] [ l0 : 0/1 ] =>* [ bad : X' ] .
maude/examples/figure-4a.maude 0 → 100644
+ 42
− 0
View file @ bca957fc
--- Bad can be reached (after several loops between l0 and l1)
load ../analysis .
mod BAD is
extending ANALYSIS .
ops l0 l1 bad : -> Location [ctor] .
ops act : -> Action [ctor] .
ops auto : -> Agent [ctor] .
ops x y : -> Clock [ctor] .
op auto : -> Automaton .
eq auto = < auto | (@ l0 inv true :
(when x >= 5 local act do { nothing } goto l1)),
(@ l1 inv (x <= 10) :
(when true local act do { x := 0 } goto l0 ,
when (y >= 50) local act goto bad)),
(@ bad inv true :
(empty))
> .
op init : -> State .
eq init = { auto }
< tick: tickOk
locs: auto @ l0
clocks: (x : 0 , y : 0)
parameters: empty
dvariables: empty
constraint: true
n: 1
>
.
endm
eof
--- set print attribute on .
--- search [1] init =>* { NET } < tick: tickNotOk locs: (auto @ bad) clocks: CLOCKS parameters: PARAMS dvariables: DVARS constraint: C n: N > .
red synthesis [1] in 'BAD : init => (auto @ bad) .
maude/examples/figure-4b.maude 0 → 100644
+ 41
− 0
View file @ bca957fc
--- Folding is needed (there are finitely many symbolic states)
load ../analysis .
mod MODEL is
extending ANALYSIS .
ops l0 l1 bad : -> Location [ctor] .
ops act : -> Action [ctor] .
ops auto : -> Agent [ctor] .
ops x : -> Clock [ctor] .
op auto : -> Automaton .
eq auto = < auto | (@ l0 inv true :
(when x >= 5 local act do { nothing } goto l1)),
(@ l1 inv (x <= 10) :
(when true local act do { x := 0 } goto l0 ,
when (x >= 11) local act goto bad)),
(@ bad inv true :
(empty))
> .
op init : -> State .
eq init = { auto }
< tick: tickOk
locs: auto @ l0
clocks: (x : 0 )
parameters: empty
dvariables: empty
constraint: true
n: 1
>
.
endm
eof
--- set print attribute on .
--- search [1] init =>* { NET } < tick: tickOk locs: (auto @ bad) clocks: CLOCKS parameters: PARAMS dvariables: DVARS constraint: C n: N > .
red search-folding in 'MODEL : init => (auto @ bad) .
maude/examples/fischer.maude 0 → 100644
+ 77
− 0
View file @ bca957fc
--- Fisher Mutual Exclusion Problem
load ../analysis .
mod FISCHER is
extending ANALYSIS .
var N : Nat .
ops obs-obs idle active check access-l cs : Nat -> Location [ctor] .
ops obs-waiting obs-violation : -> Location [ctor] .
ops exit try update no-access access enter : Nat -> Action [ctor] .
op process : Nat -> Agent [ctor] .
op observer : -> Agent [ctor] .
op turn : -> DVariable [ctor] .
ops x : Nat -> Clock [ctor] .
ops delta gamma : -> Parameter [ctor] .
op proc : Nat -> Automaton .
eq proc(N) =
< process(N) | (
(@ idle(N) inv true :
(when (turn = -1) local try(N) do {x(N) := 0} goto active(N))),
(@ active(N) inv (x(N) <= delta) :
(when true local update(N) do {x(N) := 0 ; turn := N} goto check(N))),
(@ check(N) inv true :
(when ( (turn != N) and (x(N) >= gamma)) local no-access(N) do { nothing } goto idle(N) ,
when ( (turn = N) and (x(N) >= gamma)) local access(N) do { nothing } goto access-l(N))) ,
(@ access-l(N) inv true :
(when true sync enter(N) do { nothing } goto cs(N))),
(@ cs(N) inv true :
(when true sync exit(N) do { turn := -1 } goto idle(N)))) > .
op observer : -> Automaton .
eq observer =
< observer |
(@ obs-waiting inv true :
( (when true sync enter(1) do {nothing} goto obs-obs(1)) ,
(when true sync enter(2) do {nothing} goto obs-obs(2)))) ,
(@ obs-obs(1) inv true :
( ( when true sync enter(2) do {nothing} goto obs-violation),
( when true sync exit(1) do {nothing} goto obs-waiting))),
(@ obs-obs(2) inv true :
( ( when true sync enter(1) do {nothing} goto obs-violation),
( when true sync exit(2) do {nothing} goto obs-waiting))),
(@ obs-violation inv true : empty ) > .
op init-constraint : -> BoolExpr .
eq init-constraint =
rr(var(gamma)) >= 0 and
rr(var(delta)) >= 0 .
op init : -> State .
eq init = { observer, proc(1), proc(2) }
< tick: tickOk
locs: (process(1) @ idle(1), process(2) @ idle(2), observer @ obs-waiting)
clocks: (x(1) : 0 , x(2) : 0)
parameters: (
gamma : rr(var(gamma)),
delta : rr(var(delta)))
dvariables: turn : -1
constraint: init-constraint --- and rr(var(gamma)) > rr(var(delta))
n: 1 > .
endm
eof
--- set print attribute on .
--- EF(observer @ violation)
red synthesis [1] in 'FISCHER : init => (observer @ obs-violation) .
--- EF(observer @ violation) using folding
red search-folding [1] in 'FISCHER : init => (observer @ obs-violation) .
--- Computing the whole PZG
red search-folding in 'FISCHER : init .
--- Synthesizing
red synthesis-folding in 'FISCHER : init => (observer @ obs-violation) .
--- If gamma > delta, the answer is no
red search-folding [1] in 'FISCHER : init => (observer @ obs-violation) .
maude/examples/train-intruder.maude 0 → 100644
+ 182
− 0
View file @ bca957fc
***(
Train Example in
Étienne André, Michal Knapik, Wojciech Penczek, Laure Petrucci:
Controlling Actions and Time in Parametric Timed Automata. ACSD 2016: 45-54
The integer variable choice is used to determine the choice of the intruder
*)
load ../analysis .
mod TRAIN is
--- extending SEMANTICS-FME .
extending ANALYSIS .
--- Locations
ops inittrain initgate initintruder : -> Location [ctor] . --- initial states
ops far approaching verynear gone crash : -> Location [ctor] . --- For the train
ops choosing walkingsensor walkinghouse intruderdone : -> Location [ctor] . --- for the intruder
ops up waiting nopower emergencylowering lowering down : -> Location [ctor] . --- for the gate
--- Actions
ops sensorfar sensorclose pass powercut : -> Action [ctor] .
ops choosesensor choosehouse breaksensor noaction : -> Action [ctor] .
ops startlowering endlowering : -> Action [ctor] .
--- Agents
ops train intruder gate : -> Agent [ctor] .
--- Clocks
ops xtrain xintruder xgate : -> Clock [ctor] .
--- Parameters
ops pfar papproaching pverynear pwalkingsensor pwalkinghouse : -> Parameter .
ops pwaiting plowering pemergencywaiting pemergencylowering : -> Parameter .
--- Discrete variables
op choice : -> DVariable [ctor] . --- for the strategy
ops sensoractive gatedown : -> DVariable [ctor] .
op start : -> DVariable [ctor] . --- Implementing urgent in the intruder
--- Specification of the 3 automata
op aTrain : -> Automaton .
eq aTrain = < train |
( @ inittrain inv true :
( when (start = 1) local noaction goto far
)),
( @ far inv xtrain <= pfar :
(
when ( (xtrain = pfar) and (sensoractive = 1)) sync sensorfar do { xtrain := 0 } goto approaching ,
when ( (xtrain = pfar) and (sensoractive = 0)) local noaction do { xtrain := 0 } goto approaching
)
),
( @ approaching inv (xtrain <= (papproaching - pverynear)) :
( when ( (xtrain = (papproaching - pverynear))) sync sensorclose goto verynear)),
( @ verynear inv (xtrain <= papproaching) :
( when ( (xtrain = papproaching) and (gatedown = 1)) sync pass do {xtrain := 0} goto gone ,
when ( (xtrain = papproaching) and (gatedown = 0)) sync pass do {xtrain := 0} goto crash)
),
( @ gone inv (xtrain <= 0) : empty),
( @ crash inv (xtrain <= 0) : empty)
> .
op aIntruder : -> Automaton .
eq aIntruder = < intruder |
( @ choosing inv true : --- Note that choice =i according to the transition
( when (choice = 0) local choosesensor do { start := 1} goto walkingsensor ,
when (choice = 1) local choosehouse do { start := 1} goto walkinghouse )),
( @ walkingsensor inv (xintruder <= pwalkingsensor) :
( when (xintruder = pwalkingsensor) local breaksensor do { xintruder := 0 ; sensoractive := 0} goto intruderdone )),
( @ walkinghouse inv (xintruder <= pwalkinghouse) :
( when (xintruder = pwalkinghouse) sync powercut do { xintruder := 0 ; sensoractive := 0} goto intruderdone)
),
( @ intruderdone inv true : empty )
> .
op aGate : -> Automaton .
eq aGate = < gate |
( @ initgate inv true :
( when (start = 1) local noaction goto up
)),
( @ up inv true :
(
when true sync pass do { xgate := 0 } goto up ,
when true sync sensorclose do { xgate := 0 } goto emergencylowering ,
when true sync powercut do { xgate := 0 } goto nopower ,
when true sync sensorfar do { xgate := 0 } goto waiting )
),
( @ waiting inv (xgate <= pwaiting) :
(
when true sync sensorclose do {xgate := 0} goto emergencylowering ,
when true sync pass do {xgate := 0} goto up ,
when true sync powercut do {xgate := 0} goto nopower ,
when (xgate = pwaiting) local startlowering do {xgate := 0} goto lowering
)
),
( @ lowering inv (xgate <= plowering) :
( when true sync sensorclose goto lowering ,
when true sync powercut goto lowering ,
when (xgate = plowering) local endlowering do { xgate := 0 ; gatedown := 1 } goto down ,
when true sync pass do { xgate := 0} goto up )
),
( @ down inv true :
( when true sync sensorclose goto down ,
when true sync powercut goto down ,
when true sync pass do { xgate := 0 } goto up
)
),
( @ nopower inv (xgate <= pemergencywaiting) :
( when true sync sensorfar do { xgate := 0 } goto nopower ,
when true sync pass do { xgate := 0 } goto nopower ,
when true sync sensorclose do { xgate := 0 } goto emergencylowering ,
when (xgate = pemergencywaiting) local startlowering do { xgate := 0 } goto emergencylowering
)
),
( @ emergencylowering inv (xgate <= pemergencylowering) :
( when true sync powercut goto emergencylowering ,
when true sync sensorclose goto emergencylowering ,
when (xgate = pemergencylowering) local endlowering do {xgate := 0 ; gatedown := 1 } goto down ,
when true sync pass do {xgate := 0 } goto up
)
)
> .
--- Initial constraint for the parameters
op init-constraint : -> BoolExpr .
eq init-constraint =
--- rr(var(pfar)) >= 0 and
--- rr(var(papproaching)) >= 0 and
--- rr(var(pverynear)) >= 0 and
rr(var(pwalkingsensor)) >= 0 and
rr(var(pwalkinghouse)) >= 0 and
--- rr(var(pwaiting)) >= 0 and
--- rr(var(plowering)) >= 0 and
--- rr(var(pemergencywaiting)) >= 0 and
--- rr(var(pemergencylowering)) >= 0 and
rr(var(choice)) >= 0 and
rr(var(choice)) <= 1 and
--- Fixed values in page 9 of the paper
rr(var(pfar)) === 3/1 and
rr(var(papproaching)) === 2/1 and
rr(var(pverynear)) === 1/1 and
rr(var(pwaiting)) === 1/1 and
rr(var(pemergencywaiting)) === 1/1 and
rr(var(plowering)) === 2/1 and
rr(var(pemergencylowering)) === 1/1
.
--- Initial state
op init : -> State .
eq init = { aTrain, aIntruder, aGate }
< tick: tickOk
locs: (train @ inittrain, intruder @ choosing, gate @ initgate)
clocks: (xtrain : 0, xintruder : 0, xgate : 0)
parameters: (
pfar : rr(var(pfar)),
papproaching : rr(var(papproaching)),
pverynear : rr(var(pverynear)),
pwalkingsensor : rr(var(pwalkingsensor)),
pwalkinghouse : rr(var(pwalkinghouse)),
pwaiting : rr(var(pwaiting)),
plowering : rr(var(plowering)),
pemergencywaiting : rr(var(pemergencywaiting)),
pemergencylowering : rr(var(pemergencylowering)))
dvariables: (choice : rr(var(choice)),
sensoractive : 1,
gatedown : 0,
start : 0
)
constraint: init-constraint
n: 1 > .
endm
eof
--- EF(train in crash)
red synthesis [ 1 ] in 'TRAIN : init => (train @ crash) .
--- EF(train in crash) with folding
red search-folding in 'TRAIN : init => (train @ crash) .
--- Computing the whole PZG
red search-folding in 'TRAIN : init .
maude/fme.maude 0 → 100644
+ 405
− 0
View file @ bca957fc
--- Fourier-Motzkin Elimination for eliminating real-valued variables
fmod LINEAR-TERM is
including ALT-REAL-INTEGER-EXPR .
sort LinRTerm .
subsorts Rat RVar < LinRTerm < RExpr .
op _*_ : Rat LinRTerm -> LinRTerm [ditto] .
sort StLinRTerm .
subsorts RVar < StLinRTerm < LinRTerm StRExpr .
op _*_ : Rat StLinRTerm -> StLinRTerm [ditto] .
endfm
fmod LINEAR-EXPR is
including LINEAR-TERM .
sort LinRExpr .
subsorts LinRTerm < LinRExpr < RExpr .
op _+_ : LinRExpr LinRExpr -> LinRExpr [ditto] .
sort StLinRExpr .
subsort StLinRTerm < StLinRExpr < LinRExpr StRExpr .
op _+_ : StLinRExpr LinRExpr -> StLinRExpr [ditto] .
endfm
fmod REL-LINEAR-EXPR is
including LINEAR-EXPR .
sort RelLinRExpr .
subsort Bool < RelLinRExpr < BoolExpr .
op _<_ : LinRExpr LinRExpr -> RelLinRExpr [ditto] .
op _<=_ : LinRExpr LinRExpr -> RelLinRExpr [ditto] .
op _>_ : LinRExpr LinRExpr -> RelLinRExpr [ditto] .
op _>=_ : LinRExpr LinRExpr -> RelLinRExpr [ditto] .
endfm
view RelLinRExpr from TRIV to REL-LINEAR-EXPR is
sort Elt to RelLinRExpr .
endv
fmod CONJ-REL-LIN-REAL-EXPR is
pr REL-LINEAR-EXPR .
sort ConjRelLinRExpr .
subsort RelLinRExpr < ConjRelLinRExpr < BoolExpr .
op _and_ : ConjRelLinRExpr ConjRelLinRExpr -> ConjRelLinRExpr [ditto] .
endfm
fmod POLYNOMIAL-EXPANSION is
protecting ALT-REAL-INTEGER-EXPR .
var X : RVar .
vars R R1 R2 : Rat .
vars RE RE1 RE2 : RExpr .
eq 0 + RE = RE .
eq 0 * RE = 0 .
eq 1 * RE = RE .
--- eliminate the minus operators
eq RE1 - RE2 = RE1 + (- RE2) .
eq - X = -1 * X .
eq - (- RE) = RE .
eq - (RE1 + RE2) = (- RE1) + (- RE2) .
eq - (RE1 * RE2) = (- RE1) * RE2 .
eq - (RE1 - RE2) = (- RE1) + RE2 .
eq - (RE1 / RE2) = (- RE1) / RE2 .
--- distributive law
eq RE * (RE1 + RE2) = RE * RE1 + RE * RE2 .
--- merging two terms (Note: 1 is not declared as id)
eq R1 * RE + R2 * RE = (R1 + R2) * RE .
eq R1 * RE + RE = (R1 + 1) * RE .
eq RE + RE = 2 * RE .
endfm
--- We first compute "normalized" relations of the form EXP <=/< 0.
fmod CONJ-REL-LIN-REAL-EXPR-NORMAL is
pr CONJ-REL-LIN-REAL-EXPR .
var X : RVar .
var NR : NzRat .
vars SRE : StRExpr .
vars RE RE' : RExpr .
vars CRL CRL' : ConjRelLinRExpr .
op normal : ConjRelLinRExpr ~> ConjRelLinRExpr .
eq normal(RE <= SRE and CRL) = RE + (- SRE) <= 0 and normal(CRL) .
eq normal(RE < SRE and CRL) = RE + (- SRE) < 0 and normal(CRL) .
eq normal(RE >= SRE and CRL) = SRE + (- RE) <= 0 and normal(CRL) .
eq normal(RE > SRE and CRL) = SRE + (- RE) < 0 and normal(CRL) .
eq normal(RE <= NR and CRL) = RE + (- NR) <= 0 and normal(CRL) .
eq normal(RE < NR and CRL) = RE + (- NR) < 0 and normal(CRL) .
eq normal(RE >= NR and CRL) = NR + (- RE) <= 0 and normal(CRL) .
eq normal(RE > NR and CRL) = NR + (- RE) < 0 and normal(CRL) .
eq normal(NR * X <= 0 and CRL) = if NR > 0 then X <= 0 else -1 * X <= 0 fi and normal(CRL) .
eq normal(NR * X < 0 and CRL) = if NR > 0 then X < 0 else -1 * X < 0 fi and normal(CRL) .
eq normal(NR * X >= 0 and CRL) = if NR > 0 then -1 * X <= 0 else X <= 0 fi and normal(CRL) .
eq normal(NR * X > 0 and CRL) = if NR > 0 then -1 * X < 0 else X < 0 fi and normal(CRL) .
eq normal(RE >= 0 and CRL) = - RE <= 0 and normal(CRL) [owise] .
eq normal(RE > 0 and CRL) = - RE < 0 and normal(CRL) [owise] .
eq normal(RE <= SRE) = RE + (- SRE) <= 0 .
eq normal(RE < SRE) = RE + (- SRE) < 0 .
eq normal(RE >= SRE) = SRE + (- RE) <= 0 .
eq normal(RE > SRE) = SRE + (- RE) < 0 .
eq normal(RE <= NR) = RE + (- NR) <= 0 .
eq normal(RE < NR) = RE + (- NR) < 0 .
eq normal(RE >= NR) = NR + (- RE) <= 0 .
eq normal(RE > NR) = NR + (- RE) < 0 .
eq normal(NR * X <= 0) = if NR > 0 then X <= 0 else -1 * X <= 0 fi .
eq normal(NR * X < 0) = if NR > 0 then X < 0 else -1 * X < 0 fi .
eq normal(NR * X >= 0) = if NR > 0 then -1 * X <= 0 else X <= 0 fi .
eq normal(NR * X > 0) = if NR > 0 then -1 * X < 0 else X < 0 fi .
eq normal(RE >= 0) = - RE <= 0 [owise] .
eq normal(RE > 0) = - RE < 0 [owise] .
eq normal(true and CRL) = normal(CRL) .
eq normal(false and CRL) = false .
eq normal(CRL) = CRL [owise] .
endfm
fmod FOURIER-MOTZKIN-STANDARD is
pr CONJ-REL-LIN-REAL-EXPR-NORMAL .
pr POLYNOMIAL-EXPANSION .
var NR : Rat .
var X Y : RVar .
vars RE RE1 RE2 : RExpr .
var RLE : RelLinRExpr .
vars CRL CRL' : ConjRelLinRExpr .
--- transform normalized linear inequalities containing X
op std : RVar ConjRelLinRExpr ~> ConjRelLinRExpr .
eq std(X, NR * X + RE <= 0 and CRL)
= (if NR > 0 then X + RE * (1 / NR) <= 0 else X + RE * (1 / NR) >= 0 fi) and std(X, CRL) .
eq std(X, NR * X + RE <= 0)
= (if NR > 0 then X + RE * (1 / NR) <= 0 else X + RE * (1 / NR) >= 0 fi) .
eq std(X, NR * X + RE < 0 and CRL)
= (if NR > 0 then X + RE * (1 / NR) < 0 else X + RE * (1 / NR) > 0 fi) and std(X, CRL) .
eq std(X, NR * X + RE < 0)
= (if NR > 0 then X + RE * (1 / NR) < 0 else X + RE * (1 / NR) > 0 fi) .
eq std(X, NR * X <= 0 and CRL) = (if NR > 0 then X <= 0 else X >= 0 fi) and std(X, CRL) .
eq std(X, NR * X <= 0 ) = (if NR > 0 then X <= 0 else X >= 0 fi) .
eq std(X, NR * X < 0 and CRL) = (if NR > 0 then X < 0 else X > 0 fi) and std(X, CRL) .
eq std(X, NR * X < 0 ) = (if NR > 0 then X < 0 else X > 0 fi) .
eq std(X, CRL) = CRL [owise] . --- no term containing X
endfm
fmod FOURIER-MOTZKIN is
pr FOURIER-MOTZKIN-STANDARD .
inc SET{RelLinRExpr} *
(op _,_ : Set{RelLinRExpr} Set{RelLinRExpr} -> Set{RelLinRExpr} to _;_) .
vars X Y : RVar .
vars R R1 R2 R3 : Rat .
vars RE RE1 RE2 : RExpr .
var RLE : RelLinRExpr .
var RLS RLS1 RLS2 : Set{RelLinRExpr} .
var CRL NCRL : ConjRelLinRExpr .
var KCRL : [ConjRelLinRExpr] .
--- short-circuit evaluation
op _and-then_ : ConjRelLinRExpr ConjRelLinRExpr ~> Bool [ditto] .
eq true and-then KCRL = KCRL .
eq false and-then KCRL = false .
eq CRL and-then KCRL = CRL and KCRL [owise] .
--- Fourier-Motzkin Elimination
op fme : RVar ConjRelLinRExpr ~> ConjRelLinRExpr .
eq fme(X, CRL) = elimEq(X, normal(CRL)) .
--- eliminate some equalities
op elimEq : RVar ConjRelLinRExpr ~> ConjRelLinRExpr .
eq elimEq(X, X + (-1) * Y <= 0 and (-1) * X + Y <= 0 and CRL) = subst(X, Y, CRL) . --- [print X " <- " Y] .
eq elimEq(X, X + (- R) <= 0 and (-1) * X + R <= 0 and CRL) = subst(X, R, CRL) . --- [print X " <- " R] .
eq elimEq(X, CRL) = elimEqStd(X,std(X,CRL)) [owise] .
--- eliminate more equalities
op elimEqStd : RVar ConjRelLinRExpr ~> ConjRelLinRExpr .
eq elimEqStd(X, X + RE >= 0 and X + RE <= 0 and CRL) = normal(subst(X, - RE, CRL)) . --- [print X " <- " RE] .
eq elimEqStd(X, CRL) = split(X, CRL, empty, empty) [owise] . --- [ print X " by FME"] .
--- substitute X by RE
op subst : RVar RExpr ConjRelLinRExpr ~> ConjRelLinRExpr .
eq subst(X, RE, R * X + RE1 <= 0 and CRL) = R * RE + RE1 <= 0 and subst(X, RE, CRL) .
eq subst(X, RE, X + RE1 <= 0 and CRL) = RE + RE1 <= 0 and subst(X, RE, CRL) .
eq subst(X, RE, R * X <= 0 and CRL) = R * RE <= 0 and subst(X, RE, CRL) .
eq subst(X, RE, X <= 0 and CRL) = RE <= 0 and subst(X, RE, CRL) .
eq subst(X, RE, R * X + RE1 < 0 and CRL) = R * RE + RE1 < 0 and subst(X, RE, CRL) .
eq subst(X, RE, X + RE1 < 0 and CRL) = RE + RE1 < 0 and subst(X, RE, CRL) .
eq subst(X, RE, R * X < 0 and CRL) = R * RE < 0 and subst(X, RE, CRL) .
eq subst(X, RE, X < 0 and CRL) = RE < 0 and subst(X, RE, CRL) .
eq subst(X, RE, R * X + RE1 >= 0 and CRL) = R * RE + RE1 >= 0 and subst(X, RE, CRL) .
eq subst(X, RE, X + RE1 >= 0 and CRL) = RE + RE1 >= 0 and subst(X, RE, CRL) .
eq subst(X, RE, R * X >= 0 and CRL) = R * RE >= 0 and subst(X, RE, CRL) .
eq subst(X, RE, X >= 0 and CRL) = RE >= 0 and subst(X, RE, CRL) .
eq subst(X, RE, R * X + RE1 > 0 and CRL) = R * RE + RE1 > 0 and subst(X, RE, CRL) .
eq subst(X, RE, X + RE1 > 0 and CRL) = RE + RE1 > 0 and subst(X, RE, CRL) .
eq subst(X, RE, R * X > 0 and CRL) = R * RE > 0 and subst(X, RE, CRL) .
eq subst(X, RE, X > 0 and CRL) = RE > 0 and subst(X, RE, CRL) .
eq subst(X, RE, CRL) = CRL [owise] .
--- split a set of inequalities into the three cases: X >= RE or X > RE,
--- X <= RE or X < RE, and inequalities not containing X
op split : RVar ConjRelLinRExpr Set{RelLinRExpr} Set{RelLinRExpr} ~> ConjRelLinRExpr .
eq split(X, X + RE >= 0 and CRL, RLS1, RLS2) = split(X, CRL, X + RE >= 0 ; RLS1, RLS2) .
eq split(X, X + RE > 0 and CRL, RLS1, RLS2) = split(X, CRL, X + RE > 0 ; RLS1, RLS2) .
eq split(X, X + RE <= 0 and CRL, RLS1, RLS2) = split(X, CRL, RLS1, X + RE <= 0 ; RLS2) .
eq split(X, X + RE < 0 and CRL, RLS1, RLS2) = split(X, CRL, RLS1, X + RE < 0 ; RLS2) .
eq split(X, X >= 0 and CRL, RLS1, RLS2) = split(X, CRL, X >= 0 ; RLS1, RLS2) .
eq split(X, X > 0 and CRL, RLS1, RLS2) = split(X, CRL, X > 0 ; RLS1, RLS2) .
eq split(X, X <= 0 and CRL, RLS1, RLS2) = split(X, CRL, RLS1, X <= 0 ; RLS2) .
eq split(X, X < 0 and CRL, RLS1, RLS2) = split(X, CRL, RLS1, X < 0 ; RLS2) .
eq split(X, X + RE >= 0, RLS1, RLS2) = split(X, true, X + RE >= 0 ; RLS1, RLS2) .
eq split(X, X + RE > 0, RLS1, RLS2) = split(X, true, X + RE > 0 ; RLS1, RLS2) .
eq split(X, X + RE <= 0, RLS1, RLS2) = split(X, true, RLS1, X + RE <= 0 ; RLS2) .
eq split(X, X + RE < 0, RLS1, RLS2) = split(X, true, RLS1, X + RE < 0 ; RLS2) .
eq split(X, X >= 0, RLS1, RLS2) = split(X, true, X >= 0 ; RLS1, RLS2) .
eq split(X, X > 0, RLS1, RLS2) = split(X, true, X > 0 ; RLS1, RLS2) .
eq split(X, X <= 0, RLS1, RLS2) = split(X, true, RLS1, X <= 0 ; RLS2) .
eq split(X, X < 0, RLS1, RLS2) = split(X, true, RLS1, X < 0 ; RLS2) .
eq split(X, CRL, RLS1, RLS2) = CRL and gen(reduceM(X,RLS1), reduceM(X,RLS2)) [owise] .
--- Generate new inequalities
op gen : Set{RelLinRExpr} Set{RelLinRExpr} ~> ConjRelLinRExpr .
eq gen(RLS1, empty) = true .
eq gen(empty, RLS2) = true .
eq gen(RLE ; RLS1, RLS2) = gen1(RLE,RLS2) and-then gen(RLS1,RLS2) [owise] .
op gen1 : RelLinRExpr Set{RelLinRExpr} ~> ConjRelLinRExpr .
eq gen1(X + RE1 >= 0, X + RE2 <= 0 ; RLS2) = (RE2 + (- RE1) <= 0) and-then gen1(X + RE1 >= 0, RLS2) .
eq gen1(X >= 0, X + RE2 <= 0 ; RLS2) = (RE2 <= 0) and-then gen1(X >= 0, RLS2) .
eq gen1(X + RE1 >= 0, X <= 0 ; RLS2) = ((- RE1) <= 0) and-then gen1(X + RE1 >= 0, RLS2) .
eq gen1(X >= 0, X <= 0 ; RLS2) = gen1(X >= 0, RLS2) .
eq gen1(X + RE1 >= 0, X + RE2 < 0 ; RLS2) = (RE2 + (- RE1) < 0) and-then gen1(X + RE1 >= 0, RLS2) .
eq gen1(X >= 0, X + RE2 < 0 ; RLS2) = (RE2 < 0) and-then gen1(X >= 0, RLS2) .
eq gen1(X + RE1 >= 0, X < 0 ; RLS2) = ((- RE1) < 0) and-then gen1(X + RE1 >= 0, RLS2) .
eq gen1(X >= 0, X < 0 ; RLS2) = false .
eq gen1(X + RE1 > 0, X + RE2 <= 0 ; RLS2) = (RE2 + (- RE1) < 0) and-then gen1(X + RE1 > 0, RLS2) .
eq gen1(X > 0, X + RE2 <= 0 ; RLS2) = (RE2 <= 0) and-then gen1(X > 0, RLS2) .
eq gen1(X + RE1 > 0, X <= 0 ; RLS2) = ((- RE1) <= 0) and-then gen1(X + RE1 > 0, RLS2) .
eq gen1(X > 0, X <= 0 ; RLS2) = false .
eq gen1(X + RE1 > 0, X + RE2 < 0 ; RLS2) = (RE2 + (- RE1) < 0) and-then gen1(X + RE1 > 0, RLS2) .
eq gen1(X > 0, X + RE2 < 0 ; RLS2) = (RE2 < 0) and-then gen1(X > 0, RLS2) .
eq gen1(X + RE1 > 0, X < 0 ; RLS2) = ((- RE1) < 0) and-then gen1(X + RE1 > 0, RLS2) .
eq gen1(X > 0, X < 0 ; RLS2) = false .
eq gen1(RLE, empty) = true .
--- Remove some obvious intermdiate eqs
---NOTE: strict operators are rarely used, so we omit reduction for them
op reduceM : RVar Set{RelLinRExpr} ~> Set{RelLinRExpr} .
ceq reduceM(X, X + R1 * Y + RE <= 0 ; X + R2 * Y + RE <= 0 ; X + R3 * Y + RE <= 0 ; RLS)
= reduceM(X, X + R1 * Y + RE <= 0 ; X + R2 * Y + RE <= 0 ; RLS)
if R1 <= R3 /\ R3 <= R2 .
ceq reduceM(X, X + R1 * Y <= 0 ; X + R2 * Y <= 0 ; X + R3 * Y <= 0 ; RLS)
= reduceM(X, X + R1 * Y <= 0 ; X + R2 * Y <= 0 ; RLS)
if R1 <= R3 /\ R3 <= R2 .
ceq reduceM(X, X + R1 * Y + RE >= 0 ; X + R2 * Y + RE >= 0 ; X + R3 * Y + RE >= 0 ; RLS)
= reduceM(X, X + R1 * Y + RE >= 0 ; X + R2 * Y + RE >= 0 ; RLS)
if R1 <= R3 /\ R3 <= R2 .
ceq reduceM(X, X + R1 * Y >= 0 ; X + R2 * Y >= 0 ; X + R3 * Y >= 0 ; RLS)
= reduceM(X, X + R1 * Y >= 0 ; X + R2 * Y >= 0 ; RLS)
if R1 <= R3 /\ R3 <= R2 .
eq reduceM(X, RLS) = RLS [owise] .
endfm
eof
fmod TEST-FME is
protecting FOURIER-MOTZKIN .
vars X Y Z : RVar .
endfm
---(
red - ((X * (Y + 1)) * (X + 1)) .
red (X + Y) * (X - Y) .
red 1 + X * (-3 + X * (4 + X * (0 + X * (-12 + X * 2)))) .
red X + X + X + X + Y + Y + Y + 2 * X .
red (X + Y) * (X + Y) * (X + Y) .
red std(X, normal(X + Y >= 0 and 2 * X + Y >= 2)) .
red std(X, normal(- X + Y >= 1 and - X + 2 * Y >= -1)) .
---)
red fme(X, 2 * X + 5 * Y + - 4 * Z <= 10
and 3 * X + - 6 * Y + 3 * Z <= 9
and - X + 5 * Y + - 2 * Z <= - 7
and - 3 * X + 2 * Y + 6 * Z <= 12) .
red fme(Y,
fme(X, 2 * X + 5 * Y + - 4 * Z <= 10
and 3 * X + - 6 * Y + 3 * Z <= 9
and - X + 5 * Y + - 2 * Z <= - 7
and - 3 * X + 2 * Y + 6 * Z <= 12)) .
red fme(Z,
fme(Y,
fme(X, 2 * X + 5 * Y + - 4 * Z <= 10
and 3 * X + - 6 * Y + 3 * Z <= 9
and - X + 5 * Y + - 2 * Z <= - 7
and - 3 * X + 2 * Y + 6 * Z <= 12))) .
---
red fme(X, X + (Y - 2 * Z) >= 2
and Z - X - 3 * Y >= 0
and Y + Z >= 1) .
red fme(Y,
fme(X, X + (Y - 2 * Z) >= 2
and Z - X - 3 * Y >= 0
and Y + Z >= 1)) .
red fme(Z,
fme(Y,
fme(X, X + (Y - 2 * Z) >= 2
and Z - X - 3 * Y >= 0
and Y + Z >= 1))) .
---
red fme(X, X + Y >= 0
and 2 * X + Y >= 2
and - X + Y >= 1
and - X + 2 * Y >= -1) .
red fme(Y,
fme(X, X + Y >= 0
and 2 * X + Y >= 2
and - X + Y >= 1
and - X + 2 * Y >= -1)) .
---
red fme(X, X + Y + 2 * Z >= 1
and - X + Y + Z >= 2
and (X - Y) + Z >= 1
and - Y - 3 * Z >= 0) .
red fme(Y,
fme(X, X + Y + 2 * Z >= 1
and - X + Y + Z >= 2
and (X - Y) + Z >= 1
and - Y - 3 * Z >= 0)) .
red fme(Z,
fme(Y,
fme(X, X + Y + 2 * Z >= 1
and - X + Y + Z >= 2
and (X - Y) + Z >= 1
and - Y - 3 * Z >= 0))) .
red fme(X, 2 * X <= 10) .
red fme(X, X + 5 * Y <= 10) .
red fme(X, - X <= 10) .
red fme(X, 10 <= - X) .
--- This one fails!
red fme(X, (0).Zero <= (10).NzNat + (-1).NzInt * X and (0).Zero >= (-1).NzInt * X) .
maude/meta-pta.maude deleted 100644 → 0
+ 0
− 295
View file @ a56eab5a
***(
META-PTA
--------
This module defines "reachability", an operation that performs a fixpoint
computation accumulating the reachable states with folding, collapsing
the states that have been already visited. Due to the meta-level
operations, this module protects MODEL, the specification of the PTA.
NOTES:
- The name of the module specifying the PTA must be MODEL ( see pta-module
below )
- The function applySubstitution is implemented in Maude 3.2 (but not in 3.0)
- The function simplifyFormula is only available on Maude-SE https://maude-se.github.io/
- This module assumes that the rules specifying the behavior of the PTA
moves from DStates to NStates and vice-versa (see pta-base)
- For using the command that stops when a given location is reached, the module
defining the PTA must define the equations for the operator get-location
(see pta-base)
The global behavior is represented by a term of the form {{RS},{FS},N} where:
- RS is the set of reachable constraints (already visited)
- FS is the "frontier", i.e., the new states after performing one step of
rewriting (tick + transition)
- N is the number of fresh SMT variables created so far
This module provides 3 different reachability commands
- reachability( C | t) computing the set of all reachable states from the
constrained term C | t (representing a symbolic state of the PTA)
- reachability ( (C | t), n) same as before but bound to n steps
- reachability(l, (C | t)) stops the computation if the location l is
reached
*)
mod META-PTA is
pr MODEL .
pr META-LEVEL .
--- Global state with the set of reachable states together with a natural
--- indicating the last SMT variable created
sort GlobalState .
op {{_},_} : TermList Nat -> GlobalState .
--- The first parameters is the already visited stated
--- The second parameters is the frontier
op {{_},{_},_} : TermList TermList Nat -> GlobalState .
--- The extra parameter is the location we are looking for
op {_,{_},{_},_} : Location TermList TermList Nat -> GlobalState .
op error : -> GlobalState .
--- The module defining the PTA (whose name must be MODEL)
op pta-module : -> Module [memo] .
eq pta-module = toConstrained-rules(upModule('MODEL, false)) .
--- Module including the meta-definitions
op meta-module : -> Module [memo] .
eq meta-module = upModule('META-PTA, false) .
--- ----------------------------
vars T T' : Term .
vars T1 T2 : Term .
vars LT LT' : TermList .
vars GT GT' : TermList .
vars X Y : Term .
var S : Substitution .
var S? : Substitution? .
vars n m count k : Nat .
vars C1 C2 : Term .
var SR : SmtResult? .
var Loc : Term .
var St : State .
var B B' : Boolean .
var SCt : SCTerm .
var Ct : CTerm .
var M : Module .
vars R R' : Rule .
var RS RS' : RuleSet .
vars t t' : Term .
var tc tc' : Term .
var Ats : AttrSet .
var Cond : Condition .
vars GS GS' : GlobalState .
var l : Location .
--- ----------------------------
--- Transforming a module with conditional rules to a one with constrained terms
op toConstrained-rules : Module -> Module [memo] .
eq toConstrained-rules(M)
= (mod 'MOD-COND is
getImports(M)
sorts getSorts(M) .
getSubsorts(M)
getOps(M)
getMbs(M)
none --- No equations are allowed to perform smt-search
transform-rules(getRls(M))
endm) .
op transform-rules : RuleSet -> RuleSet .
op transform-rules : RuleSet RuleSet -> RuleSet .
eq transform-rules(RS) = transform-rules(RS, none) .
eq transform-rules(none, RS') = RS' .
eq transform-rules( R RS, RS' ) = transform-rules(RS, transform-rule(R) RS') .
--- From l = > r if phi to C | t -> C and phi | r
op transform-rule : Rule -> Rule .
eq transform-rule(rl t => t' [ Ats ] . )
= (rl '_|_[t, 'C:Boolean] => '_|_[t', 'C:Boolean] [ Ats ] .) .
--- All the conditions are assumed to be of the form C = true
eq transform-rule(crl t => t' if (tc = 'true.Boolean) [ Ats ] . )
= (rl '_|_[t, 'C:Boolean] => '_|_[t', '_and_['C:Boolean, tc]] [ Ats ] .) .
--- A generic goal for the metaSearch procedue
op fresh-goal : -> Term .
eq fresh-goal = '$NS:DCTerm .
--- A unique rule adding new states when they are not already subsumed by
--- another state
crl [step] : {{LT}, {LT'}, m} =>
{{LT, LT'}, {GT'}, k}
if LT' =/= empty /\
{{GT}, k}:= next-frontier(LT', fresh-goal, m) /\ --- one step
GT' := subsumesL( (LT, LT'), GT) /\ --- filtering
GT' =/= empty --- the result is not empty
.
--- A similar rule when we are looking for a location l
crl [step] : {l, {LT}, {LT'}, m} =>
if location-in(l, (GT', LT'))
then {l, {LT, LT', GT'}, {empty}, k} --- location found
else {l, {LT, LT'}, {GT'}, k}
fi
if LT' =/= empty /\
{{GT}, k}:= next-frontier(LT', fresh-goal, m) /\ --- one step
GT' := subsumesL( (LT, LT'), GT) /\ --- filtering
GT' =/= empty
.
--- Checking if a location is in the new frontier
op location-in : Location TermList -> Bool .
eq location-in(l, empty) = false .
eq location-in( l, (T, LT)) = l == get-location(downTerm(T, error))
or-else location-in(l, LT) .
op get-location : CTerm -> Location .
eq get-location( (S:State | B:Boolean) ) = get-location(S:State) .
--- Subsumption procedure
--- Checking if the new state (T1) is subsumed by the already present T2
--- n is used to range over all possible mathches
ceq subsumes('_|_[T1, C1], '_|_[T2, C2], n) =
if S? == noMatch
then false
else
checkImplication(C1, applySubstitution(pta-module, C2, S?))
or-else subsumes('_|_[T1, C1], '_|_[T2, C2], n + 1 )
fi
if
S? := metaMatch(pta-module, T2, T1, nil, n) --- Matching the terms
.
--- Checking the subsubtion relation between two states (represented as terms)
op subsumes : Term Term -> Bool .
op subsumes : Term Term Nat -> Bool .
eq subsumes(T1, T2) = subsumes(T1, T2, 0) .
--- Lifting the previous definition to list of constrained terms
op subsumesL : TermList TermList -> TermList .
eq subsumesL(LT, empty) = empty .
eq subsumesL(LT, (T1, GT)) =
if $subsumesL(LT, T1) == false
then (T1, subsumesL(LT, GT))
else subsumesL(LT, GT)
fi
.
op $subsumesL : TermList Term -> Bool .
eq $subsumesL(empty, T1) = false .
eq $subsumesL((T2, LT), T1) = subsumes(T1, T2) or-else $subsumesL(LT, T1) .
--- Checking the implication on constraints
op checkImplication : Term Term -> Bool .
eq checkImplication(C1, C2) =
metaCheck(pta-module, 'not_['_implies_[C1, C2]]) == false .
--- Checking if the constraint in a (constrained) term is sat
op check-constraint : Term -> Bool .
eq check-constraint('_|_[T1, C1]) =
metaCheck(pta-module, C1) .
--- One step of computation in the PTA
op step : Term Term Nat Nat -> SmtResult? .
eq step(T, T' , m, count ) = metaSmtSearch(pta-module,
T,
T',
nil,
'+,
m,
2, --- allowing one transition plus the tick
count) .
--- One step of computation generating all the successor states
op next-frontier : TermList Term Nat -> GlobalState .
op next-frontier : TermList Term Nat GlobalState -> GlobalState .
eq next-frontier(LT, T2, n) = next-frontier(LT, T2, n, {{empty}, n}) .
eq next-frontier(empty, T2, n, GS') = GS' .
ceq next-frontier((T1, LT), T2, n, GS') =
next-frontier(LT, T2, m, {{ GT}, m})
if { {GT}, m} := steps(T1,T2, 0, GS') .
op steps : Term Term Nat GlobalState -> GlobalState .
ceq steps(T1, T2, count, {{LT},n}) =
if check-constraint(T')
then steps(T1, T2, count + 1 , {{ LT, T'},m})
else steps(T1, T2, count + 1, {{ LT}, m})
fi
if { T' , S , Y , m } := step(T1, T2, n , count) .
eq steps(T, T', count, {{LT}, n}) = {{LT}, n} [owise] .
--- Defining the reachability commands
--- Unbounded reachability (until fixpoint)
op reachability : CTerm -> SCTerm .
--- Reachability with a given location
op reachability : Location CTerm -> SCTerm .
--- Computing n steps in the reachability analysis
op reachability : CTerm Nat -> SCTerm .
ceq reachability(C:CTerm, n) =
to-constrainted-terms(( GT, LT))
if {{GT}, { LT}, m} := $reachability(C:CTerm, n) .
ceq reachability(C:CTerm) =
to-constrainted-terms(( GT, LT))
if {{GT}, { LT}, m} := $reachability(C:CTerm, unbounded) .
ceq reachability(l, C:CTerm) =
to-constrainted-terms(( GT, LT))
if {l, {GT}, { LT}, m} := $reachability(l, C:CTerm ) .
op $reachability : CTerm Bound -> GlobalState .
op $reachability : Location CTerm -> GlobalState .
ceq $reachability( C:CTerm , b:Bound) = downTerm(T:Term , error)
if
{T:Term , Ty:Type} := metaRewrite(
meta-module,
upTerm({{empty}, {upTerm(C:CTerm)},0}),
b:Bound) .
ceq $reachability(l, C:CTerm ) = downTerm(T:Term , error)
if
{T:Term , Ty:Type} := metaRewrite(
meta-module,
upTerm({l, {empty}, {upTerm(C:CTerm)},0}),
unbounded) .
--- From meta-level terms to constrained-terms
op to-constrainted-terms : TermList -> SCTerm .
eq to-constrainted-terms( T1) = downTerm(T1, error) .
ceq to-constrainted-terms( (T1, LT) ) = to-constrainted-terms(T1) ;; to-constrainted-terms(LT)
if LT =/= empty .
--- simplifying constraints (only on Maude-SE)
--- op simplify : SCTerm -> SCTerm .
--- eq simplify(< St | B >) = < St | simplifyFormula(B) > .
--- eq simplify( Ct ;; SCt) = simplify(Ct) ;; simplify(SCt) .
*** utility function (don't needed in Maude 3.2)
--- op applySubstitution : Module Term Substitution -> Term .
--- eq applySubstitution(M:Module, T:Term, S:Substitution) =
--- getTerm(metaNormalize(M:Module, $applySubstitution(T:Term, S:Substitution))) .
--- op $applySubstitution : NeTermList Substitution -> Term .
--- eq $applySubstitution(V:Variable, (V:Variable <- T:Term ; S:Substitution)) = T:Term .
--- eq $applySubstitution(Q:Qid[TL:NeTermList], S:Substitution) =
--- Q:Qid[$applySubstitution(TL:NeTermList, S:Substitution)] .
--- eq $applySubstitution((T:Term, TL:NeTermList), S:Substitution) =
--- $applySubstitution(T:Term, S:Substitution), $applySubstitution(TL:NeTermList, S:Substitution) .
--- eq $applySubstitution(Q:Qid, S:Substitution) = Q:Qid [owise] .
endm
maude/pta-base.maude deleted 100644 → 0
+ 0
− 61
View file @ a56eab5a
***(
pta-base.maude
--------------
The module MODEL-BASE must be imported by the module defining the rules
of the PTA at hand.
The following sorts are defined:
- NState : a state where it is possible to perform a delay transition
- DState : the resulting state after a delay transition
- State : for delayed and non-delayed states
- Location : locations of the PTA
- DCTerm : constrained terms of the form t | C where C is a Boolean
expression and t a term of sort DState
- NCTerm : constrained terms of the form t | C where C is a Boolean
expression and t a term of sort NState
- CTerm : for constrained terms of the form t | C
- SCTerm : for sets of CTerm (used in the outputs of the analyses)
States of the system are user defined constructors of sort State
In order to use the new implemented command reachability (see meta-pta),
the definition of the PTA must implement equations (not used for
smt-search) to define the operator get-location.
*)
load smt .
--- load smt-check . --- MaudeSE
mod MODEL-BASE is
--- States
sorts State DState NState .
subsort DState NState < State .
--- Locations
sort Location .
--- Constrained terms
sort CTerm DCTerm NCTerm .
subsort DCTerm NCTerm < CTerm .
--- Lists of constrained terms
sort SCTerm .
subsort CTerm < SCTerm .
op error : -> SCTerm . --- For meta-level operations
--- Constrained terms
op _|_ : DState Boolean -> DCTerm [prec 99 format(n d d d )].
op _|_ : NState Boolean -> NCTerm [prec 99 format(n d d d )].
--- This symbol is only used to build the final solution (from meta-term
--- to terms in the sort CTerm (see ./meta-pta.maude)
op _;;_ : SCTerm SCTerm -> SCTerm [ctor assoc ] .
--- This operation must be implemented by the PTA at hand
--- it is only needed for the new command reachability
op get-location : State -> Location .
endm
maude/semantics.maude 0 → 100644
+ 174
− 0
View file @ bca957fc
***(
------------------
SYMBOLIC SEMANTICS
------------------
- NPTAD-INTERPRETER: Symbolic semantics without any simplification
- NPTAD-INTERPRETER-FME: Eliminating unused tick variables in local and binary transitions
*)
load state .
mod NPTAD-INTERPRETER is
pr STATE .
--- ---------------------------------------------
var N : Nat .
var TS : TickState .
vars L1 L2 L1' L2' : Location .
var ACT : Action .
var AG AG1 AG2 : Agent .
vars RESET RESET1 RESET2 : Resets .
vars G G1 G2 INV INV1 INV2 : Constraint .
vars R1 R2 : RExpr .
vars R T : RExpr .
var TRANS TRANS1 TRANS2 : SetTransition .
var CVALUES CVALUES' : SetClockValuation .
var DVVALUES DVVALUES' : SetDVarValuation .
var PVALUES PVALUES' : SetParValuation .
var LOCS LOCS' : SetLocValuation .
var NET : Network .
var SSTDEF SSTDEF1 SSTDEF2 : SetStateDef .
vars CONS CONS' : BoolExpr .
--- ---------------------------------------------
--- Rules
crl [tick] :
{ NET }
< tick: tickOk locs: LOCS clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >
=>
{ NET }
< tick: tickNotOk locs: LOCS clocks: CVALUES' parameters: PVALUES dvariables: DVVALUES constraint: CONS' n: (N + 1) >
if T := rr(tvar(N)) /\
CVALUES' := +time(T, CVALUES) /\ --- Advancing time
CONS' := CONS and T >= 0 and
inv(NET, LOCS, CVALUES', PVALUES, DVVALUES) /\ --- invariant on time +T
smtCheck(CONS')
.
crl [local] :
{ NET, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickNotOk locs: (AG @ L1, LOCS)
clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >
=>
{ NET, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickOk locs: (AG @ L1', LOCS)
clocks: CVALUES' parameters: PVALUES dvariables: DVVALUES' constraint: CONS' n: N >
if
CVALUES' := reset-clocks(RESET, CVALUES) /\
DVVALUES' := reset-dvars(RESET, DVVALUES) /\
--- Guard evaluated with the current values and the invariant at L1' with the new values
CONS' := CONS and
eval(G, CVALUES, PVALUES, DVVALUES) and
inv( ( NET, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > ),
(AG @ L1') , CVALUES', PVALUES, DVVALUES') /\
smtCheck(CONS')
.
crl [binary] :
{ NET, < AG1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AG2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > }
< tick: tickNotOk locs: (AG1 @ L1, AG2 @ L2, LOCS)
clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >
=>
{ NET, < AG1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AG2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > }
< tick: tickOk locs: (AG1 @ L1', AG2 @ L2', LOCS)
clocks: CVALUES' parameters: PVALUES dvariables: DVVALUES' constraint: CONS' n: N >
if
CVALUES' := reset-clocks(RESET2, reset-clocks(RESET1, CVALUES)) /\
DVVALUES' := reset-dvars(RESET2, reset-dvars(RESET1, DVVALUES)) /\
--- both guards evaluated at the current values and the two invariants with the new values
CONS' := CONS and
eval(G1, CVALUES, PVALUES, DVVALUES)
and eval(G2, CVALUES, PVALUES, DVVALUES)
and inv( ( NET, < AG1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AG2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > ),
(AG1 @ L1', AG2 @ L2'), CVALUES', PVALUES, DVVALUES') /\
smtCheck(CONS')
.
endm
mod NPTAD-INTERPRETER-FME is
pr STATE .
--- ---------------------------------------------
var N : Nat .
var TS : TickState .
vars L1 L2 L1' L2' : Location .
var ACT : Action .
var AG AG1 AG2 : Agent .
vars RESET RESET1 RESET2 : Resets .
vars G G1 G2 INV INV1 INV2 : Constraint .
vars R1 R2 : RExpr .
vars R T : RExpr .
var TRANS TRANS1 TRANS2 : SetTransition .
var CVALUES CVALUES' : SetClockValuation .
var DVVALUES DVVALUES' : SetDVarValuation .
var PVALUES PVALUES' : SetParValuation .
var LOCS LOCS' : SetLocValuation .
var NET : Network .
var SSTDEF SSTDEF1 SSTDEF2 : SetStateDef .
vars CONS CONS' : BoolExpr .
--- ---------------------------------------------
--- Rules
crl [tick] :
{ NET }
< tick: tickOk locs: LOCS clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >
=>
{ NET }
< tick: tickNotOk locs: LOCS clocks: CVALUES' parameters: PVALUES dvariables: DVVALUES constraint: CONS' n: (N + 1) >
if T := rr(tvar(N)) /\
CVALUES' := +time(T, CVALUES) /\ --- Advancing time
CONS' := CONS and T >= 0 and
inv(NET, LOCS, CVALUES', PVALUES, DVVALUES) /\ --- invariant on time +T
smtCheck(CONS')
.
crl [local] :
{ NET, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickNotOk locs: (AG @ L1, LOCS)
clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >
=>
{ NET, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > }
< tick: tickOk locs: (AG @ L1', LOCS)
clocks: CVALUES' parameters: PVALUES dvariables: DVVALUES' constraint: CONS' n: N >
if
CVALUES' := reset-clocks(RESET, CVALUES) /\
DVVALUES' := reset-dvars(RESET, DVVALUES) /\
--- Guard evaluated with the current values and the invariant at L1' with the new values
CONS' :=
fme-all( (vars-in-clocks(CVALUES) \ vars-in-clocks(CVALUES')),
CONS and
eval(G, CVALUES, PVALUES, DVVALUES) and
inv( ( NET, < AG | ( @ L1 inv INV : (when G local ACT do { RESET } goto L1' , TRANS )), SSTDEF > ),
(AG @ L1') , CVALUES', PVALUES, DVVALUES')) /\
smtCheck(CONS')
.
crl [binary] :
{ NET, < AG1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AG2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > }
< tick: tickNotOk locs: (AG1 @ L1, AG2 @ L2, LOCS)
clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >
=>
{ NET, < AG1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AG2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > }
< tick: tickOk locs: (AG1 @ L1', AG2 @ L2', LOCS)
clocks: CVALUES' parameters: PVALUES dvariables: DVVALUES' constraint: CONS' n: N >
if
CVALUES' := reset-clocks(RESET2, reset-clocks(RESET1, CVALUES)) /\
DVVALUES' := reset-dvars(RESET2, reset-dvars(RESET1, DVVALUES)) /\
--- both guards evaluated at the current values and the two invariants with the new values
CONS' :=
fme-all( (vars-in-clocks(CVALUES) \ vars-in-clocks(CVALUES')),
CONS
and eval(G1, CVALUES, PVALUES, DVVALUES)
and eval(G2, CVALUES, PVALUES, DVVALUES)
and inv( ( NET, < AG1 | ( @ L1 inv INV1 : (when G1 sync ACT do { RESET1 } goto L1' , TRANS1 )), SSTDEF1 >
, < AG2 | ( @ L2 inv INV2 : (when G2 sync ACT do { RESET2 } goto L2' , TRANS2 )), SSTDEF2 > ),
(AG1 @ L1', AG2 @ L2'), CVALUES', PVALUES, DVVALUES')) /\
smtCheck(CONS')
.
endm
maude/state.maude 0 → 100644
+ 260
− 0
View file @ bca957fc
***(
------------------
SYMBOLIC STATES
------------------
Definition of states and operations on them
*)
load syntax .
load alt-smt .
load fme .
--- Definition of the state of a PTA: values for discrete variables and clocks
--- as well as the current location for each agent/automaton
fmod VALUATION is
pr NETWORK .
pr FOURIER-MOTZKIN .
--- From parameters, clocks, variables and locations to their current values
sorts LocValuation ClockValuation ParValuation DVarValuation .
--- Current location for a given automaton/agent
op _@_ : Agent Location -> LocValuation [ctor prec 10 format(g g g o)] .
--- Current value for a clock
op _:_ : Clock RExpr -> ClockValuation [ctor prec 10] .
--- Current value for a parameter
op _:_ : Parameter RExpr -> ParValuation [ctor prec 10] .
--- Current value of a discrete variable
op _:_ : DVariable RExpr -> DVarValuation [ctor prec 10] .
endfm
view LocVal from TRIV to VALUATION is sort Elt to LocValuation . endv
view ClockVal from TRIV to VALUATION is sort Elt to ClockValuation . endv
view ParVal from TRIV to VALUATION is sort Elt to ParValuation . endv
view DVarVal from TRIV to VALUATION is sort Elt to DVarValuation . endv
view RVar from TRIV to ALT-REAL-INTEGER-EXPR is sort Elt to RVar . endv
fmod SHARED-STATE is
pr VALUATION .
pr SET{LocVal} * (sort Set{LocVal} to SetLocValuation, sort NeSet{LocVal} to NeSetLocValuation) .
pr SET{ClockVal} * (sort Set{ClockVal} to SetClockValuation, sort NeSet{ClockVal} to NeSetClockValuation) .
pr SET{ParVal} * (sort Set{ParVal} to SetParValuation, sort NeSet{ParVal} to NeSetParValuation) .
pr SET{DVarVal} * (sort Set{DVarVal} to SetDVarValuation, sort NeSet{DVarVal} to NeSetDVarValuation) .
--- Can we do tick?
sort TickState .
ops tickOk tickNotOk : -> TickState [ctor] .
--- the last n:Nat is for fresh variable generation
sort SharedState .
op < tick:_ locs:_ clocks:_ parameters:_ dvariables:_ constraint:_ n:_>
: TickState SetLocValuation SetClockValuation SetParValuation SetDVarValuation BoolExpr Nat -> SharedState [ctor format( d n d n d n d n d n d n d n d n d)] .
endfm
--- Simplification procedures using FME
fmod SMT-INTERFACE is
pr ALT-SMT-CHECK .
pr SHARED-STATE .
pr SET{RVar} * (sort Set{RVar} to SetVar, sort NeSet{RVar} to NeSetVar) .
--- IDs for SMT variables
op tvar : Nat -> SMTVarId [ctor] . --- ticks
op var : Parameter -> SMTVarId [ctor] .
op var : DVariable -> SMTVarId [ctor] .
op var : Clock -> SMTVarId [ctor] .
--- --------------------------------
vars X Y : RVar .
var B1 B2 : BoolExpr .
var Xs Xs' : SetVar .
var N : Int .
var ID : SMTVarId .
vars RE RE1 RE2 : RExpr .
var CLOCK : Clock .
var CVALUES : SetClockValuation .
--- --------------------------------
--- Extracting tvar variables from a ConjRelLinRExpr
op tvars : BoolExpr -> SetVar .
op tvars : RExpr -> SetVar .
eq tvars(true) = empty .
eq tvars(B1 and B2) = tvars(B1), tvars(B2) .
eq tvars(rr(tvar(N))) = rr(tvar(N)) .
eq tvars(RE1 <= RE2) = tvars(RE1), tvars(RE2).
eq tvars(RE1 < RE2) = tvars(RE1), tvars(RE2).
eq tvars(RE1 >= RE2) = tvars(RE1), tvars(RE2).
eq tvars(RE1 > RE2) = tvars(RE1), tvars(RE2).
eq tvars(RE1 + RE2) = tvars(RE1) , tvars(RE2) .
eq tvars(RE1 - RE2) = tvars(RE1) , tvars(RE2) .
eq tvars(RE1 * RE2) = tvars(RE1) , tvars(RE2) .
eq tvars(RE1 / RE2) = tvars(RE1) , tvars(RE2) .
eq tvars(RE1) = empty [owise] .
eq tvars(B1) = empty [owise] .
--- Extracting clock vars from ConjRelLinRExpr
op cvars : BoolExpr -> SetVar .
op cvars : RExpr -> SetVar .
eq cvars(true) = empty .
eq cvars(B1 and B2) = cvars(B1), cvars(B2) .
eq cvars(rr(var(CLOCK))) = rr(var(CLOCK)) .
eq cvars(RE1 <= RE2) = cvars(RE1), cvars(RE2).
eq cvars(RE1 < RE2) = cvars(RE1), cvars(RE2).
eq cvars(RE1 >= RE2) = cvars(RE1), cvars(RE2).
eq cvars(RE1 > RE2) = cvars(RE1), cvars(RE2).
eq cvars(RE1 + RE2) = cvars(RE1) , cvars(RE2) .
eq cvars(RE1 - RE2) = cvars(RE1) , cvars(RE2) .
eq cvars(RE1 * RE2) = cvars(RE1) , cvars(RE2) .
eq cvars(RE1 / RE2) = cvars(RE1) , cvars(RE2) .
eq cvars(RE1) = empty [owise] .
eq cvars(B1) = empty [owise] .
--- Variables in a clock expression
op vars-in-clocks : SetClockValuation -> SetVar .
eq vars-in-clocks(empty) = empty .
eq vars-in-clocks( (CLOCK : RE, CVALUES) ) = tvars(RE), vars-in-clocks(CVALUES) .
--- Eliminate a set of variable
op fme-all : SetVar BoolExpr -> BoolExpr .
eq fme-all(empty, B1) = B1 .
eq fme-all((X, Xs), B1) = fme-all(Xs, fme(X, B1)) .
--- Eliminate all the tick variables
op elim-ticks : BoolExpr -> BoolExpr .
eq elim-ticks(B1) = fme-all(tvars(B1), B1) .
--- Eliminate clock-variables and ticks
op elim-clocks : BoolExpr -> BoolExpr .
eq elim-clocks(B1) = fme-all(cvars(B1), B1) .
endfm
fmod STATE is
pr SMT-INTERFACE .
--- Global state
sort State .
op {_}_ : Network SharedState -> State [ctor] .
op error : -> State . --- For meta-level operations
--- ---------------------------------------------
var N : Nat .
var TS : TickState .
vars L1 L2 L1' L2' : Location .
var AG AG1 AG2 : Agent .
vars C1 C2 CLOCK : Clock .
vars RESET RESET1 RESET2 : Resets .
vars G G1 G2 INV INV1 INV2 : Constraint .
vars R1 R2 : RExpr .
vars R T : RExpr .
vars P1 P2 PAR : Parameter .
vars D1 D2 DVAR : DVariable .
var TRANS TRANS1 TRANS2 : SetTransition .
var CVALUES CVALUES' : SetClockValuation .
var DVVALUES DVVALUES' : SetDVarValuation .
var PVALUES PVALUES' : SetParValuation .
var LOCS LOCS' : SetLocValuation .
var NET : Network .
var SSTDEF SSTDEF1 SSTDEF2 : SetStateDef .
vars CREXPR1 CREXPR2 : ClockRExpr .
vars LINREXP1 LINREXP2 : PTA-LinRExpr .
vars CRT1 CRT2 : ClockRTerm .
var LRT : PTA-LinRTerm .
var CONS : BoolExpr .
--- ---------------------------------------------
--- --------------------
--- Operations on states
--- --------------------
op get-network : State -> Network .
eq get-network({ NET } < tick: TS locs: LOCS clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >) = NET .
op get-state : State -> SharedState .
eq get-state({ NET } < tick: TS locs: LOCS clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >) =
< tick: TS locs: LOCS clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N > .
op make-state : Network SharedState -> State .
eq make-state(NET, < tick: TS locs: LOCS clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N >) =
{ NET } < tick: TS locs: LOCS clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N > .
--- Extracting the constraint from the state
op getConstraint : State -> BoolExpr .
eq getConstraint((error).State) = false .
eq getConstraint({ NET } < tick: TS locs: LOCS clocks: CVALUES parameters: PVALUES dvariables: DVVALUES constraint: CONS n: N > ) = CONS .
--- --------------------
--- Operations on clocks
--- --------------------
--- Increase all the clocks + T
op +time : RExpr SetClockValuation -> SetClockValuation .
eq +time(T, empty) = empty .
eq +time(T, (CLOCK : R, CVALUES)) = (CLOCK : (R + T)), +time(T, CVALUES) .
--- Resetting clocks
op reset-clocks : Resets SetClockValuation -> SetClockValuation .
eq reset-clocks(nothing, CVALUES) = CVALUES .
eq reset-clocks(( DVAR := R ; RESET ), CVALUES) = reset-clocks(RESET, CVALUES) .
eq reset-clocks(( CLOCK := 0 ; RESET ), (CLOCK : R1, CVALUES)) = (CLOCK : 0), reset-clocks(RESET, CVALUES) .
--- Resetting discrete variables
op reset-dvars : Resets SetDVarValuation -> SetDVarValuation .
eq reset-dvars(nothing, DVVALUES) = DVVALUES .
eq reset-dvars( ( DVAR := R ; RESET ), (DVAR : R1 , DVVALUES)) = (DVAR : R), reset-dvars(RESET, DVVALUES) .
eq reset-dvars( ( CLOCK := 0 ; RESET ), DVVALUES ) = reset-dvars(RESET, DVVALUES) .
--- Evaluating constraints into (SMT) BoolExpr
op eval : Constraint SetClockValuation SetParValuation SetDVarValuation -> BoolExpr .
op eval : DVariable SetDVarValuation -> RExpr .
op eval : PTA-LinRTerm SetParValuation -> RExpr .
op eval : ClockRExpr SetClockValuation -> RExpr .
--- Constraints
eq eval(true, CVALUES, PVALUES, DVVALUES) = true .
eq eval(G1 and G2, CVALUES, PVALUES, DVVALUES) = eval(G1, CVALUES, PVALUES, DVVALUES) and
eval(G2, CVALUES, PVALUES, DVVALUES) .
eq eval(CREXPR1 <= LINREXP1, CVALUES, PVALUES, DVVALUES) = eval(CREXPR1, CVALUES) <= eval(LINREXP1, PVALUES) .
eq eval(CREXPR1 < LINREXP1, CVALUES, PVALUES, DVVALUES) = eval(CREXPR1, CVALUES) < eval(LINREXP1, PVALUES) .
eq eval(CREXPR1 >= LINREXP1, CVALUES, PVALUES, DVVALUES) = eval(CREXPR1, CVALUES) >= eval(LINREXP1, PVALUES) .
eq eval(CREXPR1 > LINREXP1, CVALUES, PVALUES, DVVALUES) = eval(CREXPR1, CVALUES) > eval(LINREXP1, PVALUES) .
eq eval(CREXPR1 = LINREXP1, CVALUES, PVALUES, DVVALUES) = eval(CREXPR1, CVALUES) === eval(LINREXP1, PVALUES) .
eq eval(DVAR = R, CVALUES, PVALUES, DVVALUES) = eval(DVAR, DVVALUES) === R .
eq eval(DVAR != R, CVALUES, PVALUES, DVVALUES) = eval(DVAR, DVVALUES) =/== R .
eq eval(DVAR > R, CVALUES, PVALUES, DVVALUES) = eval(DVAR, DVVALUES) > R .
eq eval(DVAR < R, CVALUES, PVALUES, DVVALUES) = eval(DVAR, DVVALUES) < R .
--- Discrete Variables
eq eval(DVAR, ((DVAR : R), DVVALUES)) = R .
--- ClockRExpr
eq eval(CLOCK, (CLOCK : R, CVALUES)) = R .
eq eval(0, CVALUES) = 0 .
eq eval(CRT1 - CRT2, CVALUES) = eval(CRT1, CVALUES) - eval(CRT2, CVALUES) .
--- Linear Terms
eq eval(LINREXP1 + LINREXP2, PVALUES) = eval(LINREXP1, PVALUES) + eval(LINREXP2, PVALUES) .
eq eval(LINREXP1 - LINREXP2, PVALUES) = eval(LINREXP1, PVALUES) - eval(LINREXP2, PVALUES) .
eq eval(PAR, ((PAR : R), PVALUES)) = R .
eq eval(R, PVALUES) = R .
eq eval(R * LRT, PVALUES) = R * eval(LRT, PVALUES) .
--- Extracting the invariants
op inv : Network SetLocValuation SetClockValuation SetParValuation SetDVarValuation -> BoolExpr .
eq inv(NET, empty, CVALUES, PVALUES, DVVALUES) = true .
eq inv( (< AG | (@ L1 inv INV : TRANS ), SSTDEF >, NET),
((AG @ L1) , LOCS) , CVALUES, PVALUES, DVVALUES) =
eval(INV, CVALUES, PVALUES, DVVALUES) and inv(NET, LOCS, CVALUES, PVALUES, DVVALUES) .
endfm
maude/syntax.maude 0 → 100644
+ 124
− 0
View file @ bca957fc
***(
-------
SYNTAX
-------
Sorts needed to represent locations, actions, clocks, parameters, etc in
networks of PTAs.
*)
--- This module needs to be *extended* with appropriate constructors
fmod BASE is
sort Location .
sorts Action .
sort Agent . --- Identifiers for automata
sort Clock .
sort Parameter .
sort DVariable . --- Discrete/integer variables
endfm
--- a*p for a:Rat and p:Parameter
fmod PTA-LINEAR-TERM is
protecting RAT .
protecting BASE .
sort PTA-LinRTerm .
subsorts Rat Parameter < PTA-LinRTerm .
op _*_ : Rat PTA-LinRTerm -> PTA-LinRTerm [ditto] .
endfm
--- b + aip1 + ... + a2pn
fmod PTA-LINEAR-EXPR is
including PTA-LINEAR-TERM .
sort PTA-LinRExpr .
subsorts PTA-LinRTerm < PTA-LinRExpr .
op _+_ : PTA-LinRExpr PTA-LinRExpr -> PTA-LinRExpr [ditto] .
op _-_ : PTA-LinRExpr PTA-LinRExpr -> PTA-LinRExpr [ditto] .
endfm
--- x1 - x2 where xi is a clock or zero
fmod CLOCK-EXPR is
including PTA-LINEAR-EXPR .
sort ClockRTerm ClockRExpr .
op 0 : -> ClockRTerm [ctor] .
subsort Clock < ClockRTerm < ClockRExpr .
op _-_ : ClockRTerm ClockRTerm -> ClockRExpr [ctor] .
endfm
--- Constructors for constraints
fmod CONSTRAINT is
pr CLOCK-EXPR .
sort Constraint .
--- Boolean operators
op true : -> Constraint [ctor] .
op _and_ : Constraint Constraint -> Constraint [ctor assoc comm] .
--- Relational operators
op _<=_ : ClockRExpr PTA-LinRExpr -> Constraint [ctor] .
op _<_ : ClockRExpr PTA-LinRExpr -> Constraint [ctor] .
op _>_ : ClockRExpr PTA-LinRExpr -> Constraint [ctor] .
op _>=_ : ClockRExpr PTA-LinRExpr -> Constraint [ctor] .
op _=_ : ClockRExpr PTA-LinRExpr -> Constraint [ctor] .
op _=_ : DVariable Rat -> Constraint [ctor] .
op _!=_ : DVariable Rat -> Constraint [ctor] .
op _<_ : DVariable Rat -> Constraint [ctor] .
op _>_ : DVariable Rat -> Constraint [ctor] .
endfm
--- Reset expressions (including changing values for discrete variables)
fmod RESET is
pr CONSTRAINT .
sort Reset .
op _:=_ : DVariable Rat -> Reset [ctor prec 20] .
op _:= 0 : Clock -> Reset [ctor prec 20] .
endfm
view Reset from TRIV to RESET is sort Elt to Reset . endv
fmod TRANSITION is
pr LIST{Reset} * (sort List{Reset} to Resets, sort NeList{Reset} to NeResets, op nil to nothing, op __ to _;_) .
--- Transitions.
sort Transition .
op when_local_do`{_`}goto_ : Constraint Action Resets Location -> Transition [ctor] .
op when_sync_do`{_`}goto_ : Constraint Action Resets Location -> Transition [ctor] .
--- Version without Resets
var A : Action .
var C : Constraint .
var L : Location .
op when_local_goto_ : Constraint Action Location -> Transition .
op when_sync_goto_ : Constraint Action Location -> Transition .
eq when C local A goto L = when C local A do { nothing } goto L .
eq when C sync A goto L = when C sync A do { nothing } goto L .
endfm
view Transition from TRIV to TRANSITION is sort Elt to Transition . endv
fmod STATE-DEF is
pr SET{Transition} * (sort Set{Transition} to SetTransition, sort NeSet{Transition} to NeSetTransition) .
--- Definition of locations with invariant and transitions
sort StateDef .
op @_inv_:_ : Location Constraint SetTransition -> StateDef [ctor] .
endfm
view StateDef from TRIV to STATE-DEF is sort Elt to StateDef . endv
--- Syntax defining locations with invariants and transitions
fmod AUTOMATON is
pr SET{StateDef} * (sort Set{StateDef} to SetStateDef, sort NeSet{StateDef} to NeSetStateDef) .
--- Automaton as a set of locations and transitions
sort Automaton .
op <_|_> : Agent SetStateDef -> Automaton [ctor] .
endfm
view Automaton from TRIV to AUTOMATON is sort Elt to Automaton . endv
fmod NETWORK is
--- Network as a set of Automata
pr SET{Automaton} * (sort Set{Automaton} to Network, sort NeSet{Automaton} to NeNetwork) .
endfm
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment