Closed matifch closed 2 years ago
Valo13
commented
3 years ago Sorry for the late reaction, but could you provide us with the examples you used to reach the out of memory issue so we could try to reproduce this (and test changes) on our end?
matifch
commented
3 years ago Formula is:
[!inactive_v_p(1)*.!inactive_v_p(2)*.!inactivate_v_p0*.(error_at(1)+error_at(2))]falseand mCRL2 code is:
sort
HB_Type = struct hb0_to_1|hb0_to_2|hb1_to_0|hb2_to_0;
map
update: HB_Type # List(Bool) -> List(Bool);
minimum: List(Nat) -> Nat;
updateTM: List(Bool) # List(Nat) #Nat -> List(Nat); % if a boolean value in list is true then respective value in tm is tmax otherwise tm /2.
assignF:List(Bool) ->List(Bool);
reciprocal:HB_Type->HB_Type;
TMAX: Nat;
TMIN: Nat;
var
n,m:Nat;
b,b1,b2:Bool;
l: List(Bool);
ln:List (Nat);
tmax:Nat;
msg:HB_Type;
eqn
msg==hb0_to_1 -> reciprocal(msg)=hb1_to_0;
msg==hb0_to_2 -> reciprocal(msg)=hb2_to_0;
msg==hb2_to_0 -> reciprocal(msg)=hb0_to_2;
msg==hb1_to_0 -> reciprocal(msg)=hb0_to_1;
msg==hb1_to_0 -> update(msg,l)=[true,l.1];
msg==hb2_to_0 -> update(msg,l)=[l.0,true];
minimum ([n])=n;
minimum (n |> (m |>ln))= min (n,minimum (m |> ln));
updateTM ([],[],tmax)=[];
updateTM (b |> l,n |> ln,tmax) = if(b==true,tmax |> updateTM(l,ln,tmax), (n div 2)|> updateTM(l,ln,tmax));
assignF([])=[];
assignF(b|>[])=[false];
assignF(b|>l)=false|>assignF(l);
TMAX=10;
TMIN=2;
act
broadcast,rcv_from_p0,broadcasting,
send_to_p,rcv_by_p, rcv_heartbeat,
respond,rcv_from_p, responding,
send_to_p0,rcv_by_p0,rcv_response: HB_Type;
lose_message: HB_Type;
inactivate_nv_p0,inactivate_v_p0, inactive_nv_p0,note_inactivate_nv_p0;
inactivate_v_p,error_at,inactive_v_p,inactivate_nv_p:Nat;
for_p_timeout,timeout_at_p,timeout_at:Nat;
tick,ticking;
error2TMAX:Nat;
a,b:Bool;
proc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Process P[0]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
P0(t,timeout:Nat,active:Bool,rcvd:List(Bool), tm:List(Nat))=
(t<timeout)-> tick.P0(t=t+1)
+
(active) -> inactivate_v_p0.P0(active=false)
+
sum hb:HB_Type.rcv_by_p0(hb).P0(rcvd=update (hb,rcvd))
+
(active && t==timeout)->
(minimum (updateTM(rcvd,tm,TMAX)) >=TMIN) -> broadcast(hb0_to_1).broadcast(hb0_to_2).
P0(0,minimum (updateTM(rcvd,tm,TMAX)),active,assignF(rcvd),updateTM(rcvd,tm,TMAX))
<> inactivate_nv_p0.P0(active=false)
;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Process for P[1..n]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
P (id:Nat,active:Bool, hb:HB_Type)=
tick.P()
+
(active) -> inactivate_v_p(id).P(active=false)
+
rcv_by_p(hb).((active) -> respond(reciprocal(hb)).P() <> P())
+
(active) -> timeout_at_p(id).inactivate_nv_p(id).error_at(id);
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Processes for SW_for_P
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Stopwatch for timeout at P[i]. If a P[i] doesn't get heartbeat of P0 for 3tmax-tmin then timeout
% signal is generated
SW_for_P (t,id:Nat,msg:HB_Type)= rcv_by_p(msg).SW_for_P(t=0)
+
inactivate_v_p(id).Idle_Ticking % volunteer inactivation
+
(t == 3*TMAX-TMIN) -> for_p_timeout(id).delta %% timeout concepr at p[1] is to become inactive after 3tmax-tmin time
<>
tick.SW_for_P(t=t+1);
Idle_Ticking=tick.Idle_Ticking;
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Stopwatch Count_2tmax sends timeout upon 2tmax time
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Count_2tmax(t,id:Nat,msg:HB_Type)=(t>2*TMAX)->error2TMAX(id).delta
<>
( tick.Count_2tmax(t=t+1)
+
note_inactivate_nv_p0.Idle_Ticking
+
rcv_by_p0(msg).Count_2tmax(t=1)
);
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Stopwatch SW_for_roundtrip forces the roundtrip delay, i.e., tmin
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
SW_for_roundtrip(t:Nat,msg:HB_Type)= tick.SW_for_roundtrip()
+
rcv_from_p0(msg).Start_Ticking_p0_to_p(0,msg)
+
rcv_from_p(msg).Start_Ticking_p_to_p0(t,msg);
Start_Ticking_p0_to_p(t:Nat,msg:HB_Type)= lose_message(msg).SW_for_roundtrip(0,msg)
+
(t<TMIN) -> (tick.Start_Ticking_p0_to_p(t=t+1)
+
send_to_p(msg).SW_for_roundtrip(t,reciprocal(msg))
)
<>
send_to_p(msg).SW_for_roundtrip(t,reciprocal(msg));
Start_Ticking_p_to_p0(t:Nat,msg:HB_Type)= lose_message(msg).SW_for_roundtrip(0,reciprocal(msg))
+
(t<TMIN) -> ( tick.Start_Ticking_p_to_p0(t=t+1)
+
send_to_p0(msg).SW_for_roundtrip(0,reciprocal(msg)) )
<>
send_to_p0(msg).SW_for_roundtrip(0,reciprocal(msg));
HeartBeat_Static=
allow( {
ticking,inactive_nv_p0,inactivate_nv_p,inactivate_v_p0,inactive_v_p,broadcasting, rcv_heartbeat, responding, rcv_response, lose_message,timeout_at,
error_at, error2TMAX
},
comm ({
tick|tick|tick|tick|tick|tick|tick|tick|tick->ticking ,
broadcast|rcv_from_p0->broadcasting,
send_to_p|rcv_by_p|rcv_by_p -> rcv_heartbeat, % from chanell to p1/p2 heartbeat
respond|rcv_from_p-> responding, % from p1/p2 to channel response HB
send_to_p0|rcv_by_p0|rcv_by_p0->rcv_response,
inactivate_v_p|inactivate_v_p->inactive_v_p,
inactivate_nv_p0|note_inactivate_nv_p0-> inactive_nv_p0,
for_p_timeout|timeout_at_p->timeout_at
},
P0(0,TMAX,true,[true,true],[TMAX,TMAX]) || P(1,true,hb0_to_1) || P (2,true,hb0_to_2) || SW_for_roundtrip(0,hb0_to_1)||SW_for_roundtrip(0,hb0_to_2)
|| SW_for_P(0,1,hb0_to_1)||SW_for_P(0,2,hb0_to_2)||Count_2tmax(1,1,hb1_to_0)||Count_2tmax(1,2,hb2_to_0)
));
init
HeartBeat_Static;I've looked into it but it seems that is is not possible to have the IDE measure the memory usage of its processes during runtime and do something (like show a prompt) when the system runs out of memory. I don't know why it gives a prompt when run via the terminal but not when run via the IDE, but I think this is inherent to the OS.
Concerning your other mentioned issues:
lps2pbes or an LTS if the PBES was created using an LTS with lts2pbes. This initial LPS or LPS should then also be supplied to pbessolve when generating counter examples. pbessolve only accepts PBESs (as INFILE), LPSs and LTSs (using -f) as input. A typo in a PBES seems unlikely, as it is generated by another tool. The tools that accept mu-calculus file are lps2pbes and lts2pbes, but these do parsing and type checking first.
In the IDE, if memory is exhausted while getting counter example, it is not prompted in the IDE. I am checking a property and it is reported false after 5 minutes but upon clicking 'C' for the counter example, neither the counter example nor the error message appears but the control return to IDE after say 10 minutes. On the hand I, I get memory exhausted error over a terminal window while checking the same property. (image attached) I am using IDE of mCRL2 toolset 202006.0 (Release) over Ubuntu (Ubuntu 20.04.2 LTS)
Few other supplementary issues are: 1) In the manual of pbes2bool, the format of the counter example is not mentioned. 2) If we make typo while giving formula file to pbes2bool, I think it is checked after generating bes equations whereas it should be checked in the beginning.
3) Manual of pbes2bool over website needs to be aligned with the one appears on the terminal. For example, "-fNAME , --fileNAME" on the website is not giving clear message as compared to "-fNAME, --file=NAME " on the help over a terminal.