# Formulating sr-latch in predicate logic.

For some time I tried formulating sr-latch behavior in predicate logic natural language for a university assignment. However there is an issue because we only can use combination logic expressions. We attempted to say that:

for every instant (t) in time it holds that:

if it holds that:
exists an instant (t1) in time before t, such that SR was set at t1
and does not exist an instant (t2) in time after t1 and before t such that SR was reset at t2
then it also holds that:
for every time instant (t3) it holds that:
if it holds that:
t3 is before t and after t1
then it also holds that:
SR outputs True

and

if it holds that:
exists an instant (t1) in time before t, such that SR was reset at t1
and does not exist an instant (t2) in time after t1 and before t such that SR was set at t2
then it also holds that:
for every time instant (t3) it holds that:
if it holds that:
t3 is before t and after t1
then it also holds that:
SR outputs False


However I quickly realized that this is a faulty formalization since if a latch would be set, and later reset (or reset, and later set) the implications wouldn't hold. But then I am not sure what I can do since we are dealing with combination logic, and while I can account for a fixed number of pairs by adding more and more parts to conjunction each having different numbers of exists statement, I certainly cant describe a general case in this way.

How can I describe the behavior of set reset latch (essentially a 1 bit memory device) using predicate logic natural language.

P.S. I understand that the format of definition is not common, but to be bluntly fair I'm more interested in overall way to approach this problem, hence i only look for explanation and don't care in which notation it would be.

Update:

I was asked to provide more structured formulation to illustrate the problem. So here is some abstract rust code which i hope clarifies things:


fn flip_flop_output(now: u64) -> bool {
for t in (now-1)..0 {
if sr_set_at(t) {
return true;
}
if sr_reset_at(t) {
return false;
}
}
}



In addition because of the way system outside of sr-latch is described it is impossible to have set and reset active at the same time, hence the order of checks does not matter in this case.

• Methodologically, first, apply a proper notation into the descriptive text to render the matter perspicuous. See what is called pseudocode in computer science as an example in this vein. Commented Jun 3, 2022 at 8:20
• @TankutBeygu could you elaborate? Do you want me to provide the formulation in pseudo code? Afaik there are no strict syntax for pseudo code. Would it be ok if i expand the question with some rust code instead? Commented Jun 3, 2022 at 8:33
• If you want to convey what you have attempted and where you are stuck easily to many readers (to yourself, too!), use at least widely familiar symbols, etc., like $t_{1} < t_{2}$ instead of 'before' and 'after'. Especially, if you consider that the subject is of electrical-electronics engineering rather than mathematics . . . Commented Jun 3, 2022 at 9:07